On Enumerating Short Projected Models

TL;DR

Two model enumeration algorithms, which adopt dual reasoning in order to shorten the found models, are presented and an adaptation of the standard conflict-driven clause learning procedure to support model enumerations without blocking clauses is presented.

Abstract

Propositional model enumeration, or All-SAT, is the task to record all models of a propositional formula. It is a key task in software and hardware verification, system engineering, and predicate abstraction, to mention a few. It also provides a means to convert a CNF formula into DNF, which is relevant in circuit design. While in some applications enumerating models multiple times causes no harm, in others avoiding repetitions is crucial. We therefore present two model enumeration algorithms, which adopt dual reasoning in order to shorten the found models. The first method enumerates pairwise contradicting models. Repetitions are avoided by the use of so-called blocking clauses, for which we provide a dual encoding. In our second approach we relax the uniqueness constraint. We present an adaptation of the standard conflict-driven clause learning procedure to support model enumeration without blocking clauses.Our procedures are expressed by means of a calculus and proofs of correctness are provided.

Figures (11)

• Figure 1: Davis-Putnam-Logemann-Loveland (DPLL) Algorithm. The main loop starts with exhaustive unit propagation. If a conflict occurs, the most recent decision is flipped. If there are no decisions left on the trail, the execution terminates returning UNSAT. If no conflict occurs and there are still unassigned variables, a decision is taken. Otherwise, the execution terminates returning SAT.
• Figure 2: CDCL-based satisfiability algorithm. In the main loop, first exhaustive unit propagation is executed. If a conflict at decision level zero occurs, the execution terminates returning UNSAT. Otherwise, the conflict is analyzed, a clause blocking the assignment responsible for the conflict is learned and backjumping occurs. If no conflict occurred and all variables are assigned, the execution terminates returning SAT, otherwise a decision is taken.
• Figure 3: Irredundant model enumeration. The black lines 1--18 and 27--28 describe ⁠ CDCL returning a model if one is found and the empty clause otherwise. Notice that for decisions, variables in ⁠ $X$ are prioritized over variables in ⁠ $(Y \cup S)$ to avoid multiple enumeration of projected models. Similarly, in line 17 it suffices to check whether no relevant decision literals are left on the trail. The blue part, i.e., lines 19--26, represents the extension to model enumeration. A second ⁠ SAT solver is called incrementally on ⁠ $N$ assuming the literals on $\pi(I, X \cup Y)$. A conflict occurs by unit propagation only, and ⁠ $\pi(I^{\star}, X \cup Y)$ is a (partial) model of ⁠ $F$. It is encoded as a dual blocking clause, and ⁠ $P$ and ⁠ $N$ are updated accordingly.
• Figure 4: The function PropagateUnits implements unit propagation in ⁠ $F$. The unit literal ⁠ $\ell$ is assigned the decision level of ⁠ $I$. If some clause ⁠ $D \in F$ containing the complement of ⁠ $\ell$ becomes falsified, PropagateUnits returns ⁠ $D$. Otherwise it returns the empty clause ⁠ $0$ indicating that no conflict has occurred. The function AnalyzeConflict is called whenever a clause ⁠ $C \in F$ becomes empty under the current assignment. It learns a clause ⁠ $D$ starting with the conflicting clause ⁠ $C$. The solver then backtracks to the second highest decision level ⁠ $j$ in ⁠ $D$ upon which ⁠$D$ becomes unit with unit literal ⁠ $\ell$, and propagates ⁠ $\ell$.
• Figure 5: Rules for projected model enumeration without repetition. States are represented as tuples $(P, N, M, I, \delta\xspace)$. The formulae ⁠ $P(X,Y,S)$ and ⁠ $N(X,Y,T)$ are a dual representation of the formula ⁠ $F(X.Y)$ whose models projected onto ⁠ $X$ are sought. These models are recorded in the initially empty ⁠ DNF ⁠ $M$. The last two elements, ⁠ $I$ and ⁠ $\delta\xspace$, denote the current trail and decision level function, respectively. If a model is found or a conflict encountered and the search space has been processed exhaustively, the search terminates (rules ⁠ End$1$ and ⁠ End$0$). Otherwise, either the model is shrunken and a dual blocking clause is added (rules ⁠ Back$1$) or conflict analysis is executed followed by non-chronological backtracking (rule ⁠ Back$0$). If the residual of ⁠ $P$ under the current trail ⁠ $I\,J$ contains a unit literal, it is propagated (rule ⁠ Unit). If none of the mentioned preconditions are met, a decision is taken. Relevant variables are prioritized (rule ⁠ DecX) over irrelevant and internal ones (rule ⁠ DecYS).

Theorems & Definitions (32)

• Example 1: Multiple model enumeration
• Example 2: Short redundant models
• Example 3: Trail and implication graph
• Example 4: Trail-based conflict-driven clause learning
• Example 5: Implication-graph-based conflict-driven clause learning
• Example 6: Projected models
• Example 7: Dual formula representation
• Example 8: Model shrinking by dual reasoning
• Proposition 1
• proof