A general purpose SAT solver.
A SAT problem consists of a set of variables and a set of clauses which must be satisfied.
A literal is either a variable (e.g.
A) or a negated variable (
A clause is a boolean expression made up of literals. e.g.
A and B and not(C)
Indicate that the problem is unsolvable, before even starting. This is a convenience feature so that clients don't need a separate code path for problems they discover during setup vs problems discovered by the solver.
Add a clause preventing more than one literal in the list from being
run_solver decider tries to solve the SAT problem. It simplifies it as much as possible first. When it
has two paths which both appear possible, it calls
decider () to choose which to explore first. If this
leads to a solution, it will be used. If not, the other path will be tried. If
we try setting the remaining variables to
decider will not be called again unless we backtrack).
Use this to tidy up at the end, when you no longer care about the order.