screwsat

A simple CDCL(Conflict-Driven-Clause-Learning) SAT Solver in Rust.
I wrote it very simple to help people(including me) understand the inside of SAT Solver.

I have implemented the core SAT Solver algorithms and techniques in screwsat.

Algorithms and Techniques

• CDCL(Conflict-Driven-Clause-Learning)
• Back Jump
• Two-Literal-Watching
• VSIDS

The performance of screwsat isn't as good as other modern sat solvers.
But you can grasp some important points of SAT Solver from screwsat(I hope).

screwsat is written in only one file and std libraries. You can use it for competitive programming problems.

Accepted by screwsat

• AtCoder Beginner Contest 187 F - Close Group
• 天下一プログラマーコンテスト2016本戦（オープンコンテスト） B - 今年の B 問題

Testing

You need to pull all SAT problems under the cnf directory that are stored by git-lfs to run cargo test.

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

How to use

screwsat can be used as a library and a command-line tool.

Command

Install

% cargo install --locked screwsat

Usage(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

Library

You need to add screwsat to Cargo.toml.

screwsat="*"

OR

Copy src/lib.rs and Paste it. (Competitive Programming Style)

Usage(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);
    }
}

Appreciation

This code is really inspired by his good simple code not522's SAT Solver

Contribution

Contributions and feedbacks are welcome. (e.g., fix typo and tedious code and my English, report bugs/issues, GIVE ME GITHUB STARS)