2. Testing satisfiability¶
To test the satisfiability of the CNF formula encoded in
a cnfgen.CNF
instance we can use the
cnfgen.CNF.is_satisfiable()
and cnfgen.CNF.solve()
methods. The former just gives a boolean answer, with the latter
provides more options about how to run the solver and returns
a satisfying assignment found in the process.
Testing satisfiability of a CNF is not at all considered to be an easy task. In full generality the problem is NP-hard [1], which essentially means that there are no fast algorithm to solve it.
In practice many formula that come from applications can be solved efficiently (i.e. it is possible to rapidly find a satisfying assignment). There is a whole community of clever software engineers and computer scientists that compete to write the fastest solver for CNF satisfiability (usually called a SAT solver) [2]. CNFgen does not implement a SAT solver, but uses behind the scenes the ones installed in the running environment. If the formula is satisfiable the value returned includes a satisfying assignment.
>>> from cnfgen import CNF
>>> F = CNF([ [1,-2], [-1] ])
>>> outcome,assignment = F.solve()
>>> outcome
True
>>> assignment == [-1,-2]
True
>>> F.add_clause([2])
>>> F.is_satisfiable()
False
It is always possible to force CNFgen
to use a specific solver or
a specific command line invocation using the cmd
parameters for
cnfgen.CNF.is_satisfiable()
. CNFgen
knows how to
interface with several SAT solvers but when the command line invokes
an unknown solver the parameter sameas
can suggest the right
interface to use.
>>> F.is_satisfiable(cmd='minisat -no-pre') # doctest: +SKIP
>>> F.is_satisfiable(cmd='glucose -pre') # doctest: +SKIP
>>> F.is_satisfiable(cmd='lingeling --plain') # doctest: +SKIP
>>> F.is_satisfiable(cmd='sat4j') # doctest: +SKIP
>>> F.is_satisfiable(cmd='my-hacked-minisat -pre',sameas='minisat') # doctest: +SKIP
>>> F.is_satisfiable(cmd='patched-lingeling',sameas='lingeling') # doctest: +SKIP
[1] | NP-hardness is a fundamental concept coming from computational complexity, which is the mathematical study of how hard is to perform certain computations. |
[2] | See http://www.satcompetition.org/ for SAT solver ranking. |