scresat

在 Rust 中实现的一个简单的 CDCL(Conflict-Driven-Clause-Learning) SAT 求解器。
我写得很简单，以便帮助人们（包括我自己）了解 SAT 求解器的内部。

我在 screwsat 中实现了核心 SAT 求解器算法和技术。

算法和技术

• CDCL(Conflict-Driven-Clause-Learning)
• 回溯
• 双文字监控
• VSIDS

screwsat 的性能不如其他现代 SAT 求解器。
但你可以从 screwsat 中（我希望）掌握 SAT 求解器的一些重要点。

screwsat 只用了一个文件和 std 库编写。你可以用它来解决算法竞赛问题。

被 screwsat 接受

• AtCoder 初级竞赛 187 F - 闭合组
• 天下一程序员竞赛 2016 总决赛（公开竞赛） B - 本年的 B 问题

测试

要运行 cargo test，需要将存储在 cnf 目录下的所有 SAT 问题拉取下来，这些问题是使用 git-lfs 存储的。

% git lfs pull
% cargo test -- --nocapture

使用方法

screwsat 可用作库和命令行工具。

命令

安装

% cargo install --locked screwsat

用法(cmd)

% screwsat --help
USAGE: screwsat [options] <input-file> [output-file]

% cat examples/sat.cnf
c Here is a comment.
c SATISFIABLE
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

% screwsat examples/sat.cnf
s SATISFIABLE
-1 -2 -3 -4 -5 0

% screwsat cnf/unsat/unsat.cnf
s UNSATISFIABLE

% screwsat examples/sat.cnf sat_result.txt
% cat sat_result.txt
SAT
-1 -2 -3 -4 -5 0

库

您需要将 screwsat 添加到 Cargo.toml。

screwsat="*"

或者

复制 src/lib.rs 并粘贴。 (算法竞赛风格)

用法(lib)

use std::vec;

use screwsat::solver::*;
use screwsat::util;
fn main() {
    {
        // Create a default Solver struct
        let mut solver = Solver::default();
        // A problem is (x1 v ¬x5 v x4) ∧ (¬x1 v x5 v x3 v x4) ∧ (x3 v x4)
        let clauses = vec![
            // (x1 v ¬x5 v x4)
            vec![Lit::from(1), Lit::from(-5), Lit::from(4)],
            // (¬x1 v x5 v x3 v x4)
            vec![Lit::from(-1), Lit::from(5), Lit::from(3), Lit::from(4)],
            // (x3 v x4)
            vec![Lit::from(3), Lit::from(4)],
        ];
        // Add clauses to solver
        clauses
            .into_iter()
            .for_each(|clause| solver.add_clause(&clause));

        let status = solver.solve(None);
        // Sat: A problem is SATISFIABLE.
        println!("{:?}", status);
        // print the assignments satisfy a given problem.
        // x1 = false x2 = false x3 = false x4 = true x5 = false
        solver.models.iter().enumerate().for_each(|(var, assign)| {
            let b = match assign {
                LitBool::True => true,
                _ => false,
            };
            print!("x{} = {} ", var + 1, b);
        });
        println!("");
    }

    {
        // Parse a DIMACS CNF file
        // c
        // c This is a sample input file.
        // c (unsatisfiable)
        // c
        // p cnf 3 5
        // 1 -2 3 0
        // -1 2 0
        // -2 -3 0
        // 1 2 -3 0
        // 1 3 0
        // -1 -2 3 0
        let input = std::fs::File::open("example/unsat.cnf").unwrap();
        let cnf = util::parse_cnf(input).unwrap();
        // 3
        let variable_num = cnf.var_num.unwrap();
        // 5
        //let clause_num = cnf.cla_num.unwrap();

        let clauses = cnf.clauses;
        // Create a new Solver struct
        let mut solver = Solver::new(variable_num, &clauses);
        let status = solver.solve(None);
        // Unsat: A problem is UNSATISFIABLE
        println!("{:?}", status);
    }

    {
        // Set the time limitation
        // You might want to set the time limitation for very hard problem
        let input = std::fs::File::open("example/hard.cnf").unwrap();
        let cnf = util::parse_cnf(input).unwrap();
        let mut solver = Solver::default();
        let clauses = cnf.clauses;
        clauses
            .into_iter()
            .for_each(|clause| solver.add_clause(&clause));
        // 5 sec
        let status = solver.solve(Some(std::time::Duration::from_secs(5)));
        // Indeterminate
        println!("{:?}", status);
    }
}

感谢

此代码确实受到了他的优秀简单代码的启发 not522 的 SAT 求解器

贡献

欢迎贡献和反馈。 （例如，修复错别字和繁琐的代码以及我的英语，报告错误/问题，给我 GitHub 星标）