An iterative model enumerator (pysat.examples.models)#
List of classes#
Enumeration procedure. |
Module description#
The module implements a simple iterative enumeration of a given number of
models of CNF or CNFPlus formula. In the latter case,
only Minicard can be used as a SAT solver. The module aims at
illustrating how one can work with model computation and enumeration.
The implementation facilitates the simplest use of a SAT oracle from the
command line. If one deals with the enumeration task from a Python
script, it is more convenient to exploit the internal model enumeration of
the pysat.solvers module. Concretely, see
pysat.solvers.Solver.enum_models().
$ cat formula.cnf
p cnf 4 4
-1 2 0
-1 3 0
-2 4 0
3 -4 0
$ models.py -e all -s glucose3 formula.cnf
v -1 -2 +3 -4 0
v +1 +2 -3 +4 0
c nof models: 2
c accum time: 0.00s
c mean time: 0.00s
Module details#
- examples.models.enumerate_models(formula, to_enum, solver, warm=False)#
Enumeration procedure. It represents a loop iterating over satisfying assignment for a given formula until either all or a given number of them is enumerated.
- Parameters:
formula (
CNFPlus) – input WCNF formulato_enum (int or 'all') – number of models to compute
solver (str) – name of SAT solver
warm (bool) – warm start flag