cnfgen.utils.solver module

SAT solver integrated with CNFgen.

Of course it does not implement an actual sat solver, but tries to use solvers installed on the machine. For the full list of supported solvers, see

cnfgen.utils.solver.supported_satsolvers

sat_solve(F, cmd=None, sameas=None, verbose=0)

Determines whether a CNF is satisfiable or not.

The satisfiability is determined using an external sat solver. If no command line is specified, the known solvers are tried in succession until one is found.

Parameters:

F: a CNF formula object

check the satisfiablility of this formula

cmd: string,optional

the actual command line used to invoke the SAT solver

sameas: string, optional

use the interface of one of the supported solvers, indicated in input. Useful when the solver ont the command line is not supported.

verbose: int

0 or less means no output. 1 shows the command line actually run. 2 outputs the solver output. (default: 0)

Returns:

A pair (answer,witness) where answer is either True when F is

satisfiable, or False otherwise. If F is satisfiable the witness

is a satisfiable assignment in form of a dictionary, otherwise it

is None.

Raises:

RuntimeError

if it is not possible to correctly invoke the solver needed.

ValueError

if sameas is set and does not match the name of a supported solver.

TypeError

if F is not a CNF object.

Examples

>>> sat_solve(F)                                               # doctest: +SKIP
>>> sat_solve(F,cmd='minisat -no-pre')                         # doctest: +SKIP
>>> sat_solve(F,cmd='glucose -pre')                            # doctest: +SKIP
>>> sat_solve(F,cmd='lingeling --plain')                       # doctest: +SKIP
>>> sat_solve(F,cmd='sat4j')                                   # doctest: +SKIP
>>> sat_solve(F,cmd='my-hacked-minisat -pre',sameas='minisat') # doctest: +SKIP
>>> sat_solve(F,cmd='patched-lingeling',sameas='lingeling')    # doctest: +SKIP

some_solver_installed(solvers=None)

Test whether we can run SAT solvers.

Parameters:

`solvername` : string / list of strings, optional

the names of the solvers to be tested.

If `solvers` is None then all supported solvers are tested.

If `solvers` is a list of strings all solvers in the list are tested.

If `solvers` is a string then only that solver is tested.

Raises:

TypeError if solvers is not of the right type.

supported_satsolvers()

List the supported SAT solvers.

Output the list of all solvers supported by CNFgen.