screwsat
A very simple CDCL(Conflict-Driven-Clause-Learning) SAT Solver in Rust
. The line of solver
is around 300
lines.
I wrote it very simple to help people(including me) understating the inside of SAT Solver.
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
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 cnf/sat/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 cnf/sat/sat.cnf
s SATISFIABLE
-1 -2 -3 -4 -5 0
% screwsat cnf/unsat/unsat.cnf
s UNSATISFIABLE
% screwsat cnf/sat/sat.cnf sat_result.txt
% cat sat_result.txt
SAT
-1 -2 -3 -4 -5 0
Library
You can add screwsat
to Cargo.toml
.
screwsat="1.0"
OR
Copy src/lib.rs
and Paste it.(Competitive Programming Style)
Usage(lib)
use std::vec;
use screwsat::solver::Solver;
use screwsat::util;
fn main() {
{
let mut solver = Solver::default();
let clauses = vec![
vec![(0, true), (4, false), (3, true)],
vec![(0, false), (4, true), (2, true), (3, true)],
vec![(2, true), (3, true)],
];
clauses
.into_iter()
.for_each(|clause| solver.add_clause(&clause));
let status = solver.solve(None);
println!("{:?}", status);
solver
.assigns
.iter()
.enumerate()
.for_each(|(var, assign)| print!("x{} = {} ", var + 1, assign));
println!("");
}
{
let cnf = util::parse_cnf("cnf/unsat/unsat.cnf").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 cnf = util::parse_cnf("examples/hard.cnf").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 simple good code not522's SAT Solver