During one of my courses SMT-solvers were discussed in quite some detail, so I wanted to apply that theory in practice myself. Currently this is only a SAT solver, but I may try to extend the functionality in the future. This isn't published as a package anywhere, since there are way better SMT-solvers such as Z3 already out there to be used in practice.
The most interesting parts of the source code are:
- The CDCL solver implementation which can efficiently solve many formulas
- The language constructs and how they are combined into a default language with specific precedences.
I've created a demo webpage in order to play with the tool using the built-in parser, which allows you to compare the performance of the 3 different solvers. It features some built-in examples in order to get an idea for the things SAT-solvers can be used for.
Currently boolean formula constructs are implemented, with related syntax
Variable
,varName
: Creates a boolean variable of the given type (currently only Boolean is supported)Not
,![a]
: Negates a boolean formulaAnd
,[a] && [b]
: Takes the conjunction of 2 or more boolean formulasOr
,[a] || [b]
: Takes the disjunction of 2 or more boolean formulasImplies
,[a] => [b]
: Takes a premise and conclusion formula, and ensures the conclusion holds if the premise holdsBiImplies
,[a] <=> [b]
: Checks whether two given formulas result in the same value
Created variables are unique, even if they use the same name, so they should be defined upfront. Below is an example of a formula in javascript:
const a = Variable("a", Bool);
const formula = And(a, Not(a));
We can also creates formulas using the parser:
const formula = parse(`a && !a`);
The formula can then be attempted to be solved using solve
:
const a = Variable("a", Bool);
const b = Variable("b", Bool);
const unsatisfiableFormula = And(a, Not(a));
const satisfiableFormula = And(Or(a, Not(b)), Or(Not(a), b));
const result1 = await unsatisfiableFormula.solve();
console.log(result1); // undefined, since no solution exists
const result2 = await satisfiableFormula.solve();
if (result2) console.log(result2.get(a), result2.get(b)); // true, true
3 satisfiability solver algorithms have been implemented:
- DavisPutnam: Wikipedia/DavisPutman
- DPLL: Wikipedia/DPLL, users.aalto.fi/DPLL
- CDCL: Wikipedia/CDCL, users.aalto.fi/CDCL, cse442-17f.github.io/CDCL
Realistically the first two shouldn't be used, since they have an exponential blowup for nearly every formula. CDCL however is relatively smart, and can be used for decently large formulas. I however haven't optimized things or applied smart heuristics to improve performance, so you still shouldn't expect amazing performance.
You can pass a specific solver when calling the solve
function on a formula:
const result2 = await satisfiableFormula.solve(DPLLSolver);
if (result2) console.log(result2.get(a), result2.get(b)); // true, true
If no solver is specified, CDCL is used.
It's not unlikely that there are mistakes in some of this code (somewhat defeating the purpose), but I've at least confirmed it behaves correctly on a couple of formulae in the form of unit tests:
https://github.com/TarVK/SAT/tree/main/src/solver/procedures/_tests
It's also relatively likely that DavisPutnam generates incorrect solutions in some cases - or even throws errors - since the algorithm to obtain the solution after satisfiability is proven, has been improvised due to a lack of sources.