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
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() {
{
let mut solver = Solver::default();
let clauses = vec![
vec![Lit::from(1), Lit::from(-5), Lit::from(4)],
vec![Lit::from(-1), Lit::from(5), Lit::from(3), Lit::from(4)],
vec![Lit::from(3), Lit::from(4)],
];
clauses
.into_iter()
.for_each(|clause| solver.add_clause(&clause));
let status = solver.solve(None);
println!("{:?}", status);
solver.models.iter().enumerate().for_each(|(var, assign)| {
let b = match assign {
LitBool::True => true,
_ => false,
};
print!("x{} = {} ", var + 1, b);
});
println!("");
}
{
let input = std::fs::File::open("example/unsat.cnf").unwrap();
let cnf = util::parse_cnf(input).unwrap();
let variable_num = cnf.var_num.unwrap();
let clauses = cnf.clauses;
let mut solver = Solver::new(variable_num, &clauses);
let status = solver.solve(None);
println!("{:?}", status);
}
{
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));
let status = solver.solve(Some(std::time::Duration::from_secs(5)));
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)