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

$ -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.

  • formula (CNFPlus) – input WCNF formula

  • to_enum (int or 'all') – number of models to compute

  • solver (str) – name of SAT solver

  • warm (bool) – warm start flag