Model Counting and Enumeration
When you determined the satisfiability of a formula with a SAT Solver and the formula is satisfiable, the solver yields one satisfying assignment (also called model) of the formula. But you might wonder how many such models there are or list them all explicitly. The first question concerns model counting, and the second concerns model enumeration.
In LogicNG, you can either determine all models for a given formula (Model Enumeration, ME), or all models for a given subset of the formula's variables (Projected Model Enumeration, PME).
Consider the following example:
solver.enumerateAllModels() returns all valid assignments of the solver:
~A, ~B, C
A, B, C
A, ~B, C
A, ~B, ~C
A, B, ~C
In case you are not interested in the model for every variable, you can give over the variables you're interested in as a parameter to the method and perform projected model enumeration. For example,
solver.enumerateAllModels(f.variable("A"), f.variable("B")) returns the possible models for the variables
solver.enumerateAllModels(f.variable("A")) returns the models for
enumerateAllModels() internally calls the solver function ModelEnumerationFunction. That is, you get the same result (here for example for the projection on
When using the solver function directly, you can perform the projected model enumeration with so-called "additional variables". Those are variables which are not relevant for the actual enumeration, but we are interested in their assignment for any found model.
Consider the following example:
SATSolver solver = MiniSat.miniSat(this.f); Formula formula1 = f.parse("A & (B | C)"); Formula formula2 = f.parse("B | D"); solver.add(formula1); solver.add(formula2); SortedSet<Variable> pmeVars = new TreeSet<>(Arrays.asList(f.variable("A"), f.variable("B"))); List<Assignment> models1 = solver.execute(ModelEnumerationFunction.builder() .variables(pmeVars) .build() ); List<Assignment> models2 = solver.execute(ModelEnumerationFunction.builder() .variables(pmeVars) .additionalVariables(f.variable("C")) .build() );
models1) returns the models:
The projected model enumeration over
B with additional variable
models2) returns the models:
A, B, ~C
A, ~B, C
That is, the projected model enumeration with additional variables finds for those assignments computed by the projected model enumeration one possible assignment for the variable
This is really just one possible assignment: Note that not only
A, B, ~C, but also
A, B, C is a valid model.
You may find
additionalVariables() useful if you want to perform projected model enumeration over
variables(), but are also interested in what truth value some "additional variables" can have in those assignments.
Note that it does not make sense to add
variables() to the builder, and it also does not make sense that the variables in
additionalVariables() and the variables in
variables() are overlapping.
Configuring the Assignment Type
The builder method
fastEvaluable() configures whether the models of the model enumeration are generated as fast evaluable Assignments or not. For details about fast evaluable assignment see the info box here.
Model counting is #P-complete, which in practice is much harder than NP. It is the task to compute the number of satisfiable models of a formula.
If you already have an algorithm for model enumeration (as you have seen above), you can trivially count the number of models:
However, this approach isn't feasible for large model counts, since every model explicitly has to be enumerated. Instead of this trivial approach, knowledge compilers can be used to compute the model count more effectively. Both, BDDs, and DNNFs are suitable for this task. The ModelCounter in LogicNG is based on the d-DNNF of a formula.
An example is:
Formula f1 = f.parse("A & (B | C)"); Formula f2 = f.parse("B | D"); Formula f3 = f.parse("~A | B & E"); List<Formula> formulas = Arrays.asList(f1, f2, f3); SortedSet<Variable> variables = new TreeSet<>(Arrays.asList(f.variable("A"), f.variable("B"), f.variable("C"), f.variable("D"), f.variable("E"))); BigInteger modelcount = ModelCounter.count(formulas, variables);
The result is 4, which can (in this simple case) be verified using model enumeration:
A, B, ~C, ~D, E
A, B, ~C, D, E
A, B, C, ~D, E
A, B, C, D, E
The second parameter of the
count function is an important one: Because of the automatic simplifications of formulas in LogicNG, it can happen that "irrelevant" variables (which don't have any influence on whether the formula is satisfiable or not) are removed from the formula. However, these variables still do affect the model count, since they can be set to both
true s.t. each of those variables increases the model count by a factor of 2. So usually it makes sense to collect the set of variables passed to the model counter not from the formula at hand, but from the source where the formula came from.
On the other hand, the set of variables must never be a strict subset of the variables of the formula.
Projected model counting is currently not implemented in LogicNG (but there are plans...).
It does not make sense to (1) compute a model, (2) perform (projected) model enumeration or (3) perform a model count when the conjunction of clauses which have been added to the solver is unsatisfiable. Depending on what you're trying to do, the result is
 (2) or
If the solver is
UNSAT, then there are two things you can do to understand why:
- Check the MUS of the SAT solver
- Check the resolution proof of the SAT solver using
unsatCore(). Careful: this method only works if you have configured your SAT solver with
proofGeneration = true
More about this in the chapter on explanations.