Add LICENSE file
Add README.md
Remove unnecessary `the`
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
LinArray
s which are threaded through the code using a linear state type (see
Control/Linear/LState.idr
).
(A recent idris2
needs to be installed and on your $PATH
)
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
weird %\n0\n\n
at the end, which needs to be removed (head -n -3
works).
The flat...
collections from that URL work out of the box.