This is a very tiny SAT solver, loosely based on this tutorial: Understanding SAT by Implementing a Simple SAT Solver in Python.
The main goal is to experiment with Idris 2's Linear Types.
The solver state (composed of watch list and current assignments) is kept in two
LinArrays which are threaded through the code using a linear state type (see
idris2 needs to be installed and on your
make && make test
Input is expected in DIMACS format, e.g.:
c This is a comment. c Lines starting with "p " contain the problem description: c Type (must be "cnf"), number of vars, number of clauses (ignored) p cnf 3 4 1 2 -3 0 2 3 0 -2 0 -1 3 0
Two very tiny test files are included, bigger samples can be obtained from e.g.:
SATLIB - Benchmark Problems.
Some of the
.cnf files there (for example the "uf..." collections) have a
%\n0\n\n at the end, which needs to be removed (
head -n -3 works).
flat... collections from that URL work out of the box.