sat

Interface for defining and solving Boolean satisfiability (SAT) problems in Rust.

Documentation

lib.rs:

Interface for defining and solving SAT problems.

The Boolean satisfiability problem (SAT for short) asks, for a given Boolean formula, whether there exists an assignment of values (true or false) to the formula's variables such that the formula evaluates to true.

SAT is NP-complete, which implies two things:

1. A large number of important problems (e.g. in program analysis, circuit design, or logistical planning) may be seen as instances of SAT.

2. It is believed that no algorithm exists which efficiently solves all instances of SAT.

The observation (1) is significant in spite of (2) because there exist algorithms (such as DPLL) which efficiently solve the SAT instances one encounters in practice.

This crate allows the user to formulate instances of SAT and to solve them using off-the-shelf SAT solvers.

// Create a SAT instance.
let mut i = sat::Instance::new();
let x = i.fresh_var();
let y = i.fresh_var();
let z = i.fresh_var();
i.assert_any(&[x, z]);        //     (x OR z)
i.assert_any(&[!x, !y, !z]);  // AND (!x OR !y OR !z)
i.assert_any(&[y]);           // AND (y = TRUE)

// Use the external program `minisat` as a solver.
let s = sat::solver::Dimacs::new(|| Command::new("minisat"));

// Solve the instance and check that it meets our requirements.
let a = s.solve(&i).unwrap();
assert!(a.get(x) || a.get(z));
assert!(!a.get(x) || !a.get(y) || !a.get(z));
assert!(a.get(y));

// Add a clause which makes the instance impossible to satisfy,
// and check that the solver recognizes as much.
i.assert_any(&[!y]);
assert!(s.solve(&i).is_none());

For a more elaborate example, see examples/petersen.rs which produces a 3-coloring of the Petersen graph.