Satsolver is a project mainly written in Python, it's free.
A simple SAT solver implemented in Python
A simple SAT solver implemented in Python (with some non-SAT abilities).
$ python repl.py 'a'
> p
= p
> p | q
= p
= q, !p
> p & !p
unsatisfiable.
> (p -> q) <=> (!p | q)
= True
A bicontional formula, a <-> b, is rewritten as (a -> b) & (b -> a).
These operators have no place in any SAT solver, but here they are anyway:
The implementation of this SAT solver is a very naïve implementation of the DPLL algorithm.
The <=>, CIRC and SM operators are written by rewriting the equations using their definitions.
This program is horribly inefficient. Do not use it.
twocolor.py shows how predicate logic can be simply used to describe a two-coloring of a graph.