Certifying Projected Knowledge Compilation

Although Boolean satisfiability (SAT) solvers serve as effective tools for many automated reasoning tasks, some applications require evaluating more detailed properties about formulas than whether or not they are satisfiable. For example, model counting [26] determines the number of satisfying assignments to a formula, while probabilistic inference [11] determines the probability that a formula will evaluate to $1$ (true), given individual probabilities that each variable is assigned value $1$. Probabilistic inference is a special case of the more general problem of weighted model counting. Generalizing to weight functions computed over algebraic semirings expands properties that can be evaluated even further [28].

Rather than implementing specialized programs for these different analysis tasks, a knowledge compiler [18, 34] converts a Boolean formula into a form for which the tasks can be performed in polynomial time, relative to the size of the representation. Most commonly, knowledge compilers generate a restricted class of Boolean formulas for which the analysis becomes tractable, such as the deterministic, decomposable, negation-normal form (d-DNNF, defined in Section 4) [18]. These formulas are encoded as directed acyclic graphs, enabling efficient sharing of common subformulas. We can therefore state the operation of a knowledge compiler as converting a Boolean formula over a set of variables $X$, denoted $\varphi (X)$, into a logically equivalent formula $\psi (X)$, such that (weighted) model counting can be performed in time polynomial in the size of $\psi$.

With projected knowledge compilation, the variables $X$ are partitioned into data variables $D$ and quantified variables $Y$, and so the input formula has the form $\varphi (D,Y)$. The task is to produce a formula $\psi (D)$ where the quantified variables have been eliminated via existential quantification. That is, the satisfying assignments of $\psi$ consist of those assignments $\alpha$ to the data variables, such that for some assignment $\beta$ to the quantified variables, their combination $\alpha \cdot \beta$ satisfies the input formula $\varphi$. This can be written as $\psi (D)\equiv \exists Y\varphi (D,Y)$. This form of projection is also referred to as “forgetting” [18, 21, 33].

The need to eliminate quantified variables arises in many contexts. For example, auxiliary variables are commonly introduced when encoding general Boolean formulas into conjunctive normal form (CNF), via either a Tseitin [38] or a Plaisted-Greenbaum [37] encoding. Although the former preserves model counts, the latter does not, and both can complicate the task of weighted model counting. As a second example, when a hardware system is described as the composition of a set of components, Boolean variables are introduced to encode the connections between components [13]. Existentially quantifying these variables abstracts away the internal system details. As a third example, a state transition system can be described via a transition relation $T(S,S^{\prime })$ defining the allowed combinations of current states $S$ and next states $S^{\prime }$ [8]. For some predicate $P(S)$ describing the current states, the quantified formula $P^{\prime }(S^{\prime })\doteq \exists S[P(S)\wedge T(S,S^{\prime })]$ describes the set of possible successor states.

Our work makes use of version 2 of the D4 knowledge compiler [30].¹¹1 Available at https://github.com/crillab/d4v2 Given a CNF file that also includes a declaration of the data variables (referred to as “show” variables), as is required for the projected model counting competitions,²²2https://mccompetition.org it will generate a d-DNNF representation of the set of data models.

For many applications of automated reasoning, including formal verification and mathematics, it is essential that the tools be fully trustworthy. In our context, there should be some method of ensuring that the output $\psi (D)$ generated by a projected knowledge compiler is truly equivalent to $\exists Y\varphi (D,Y)$. We have devised a proof framework for expressing such proofs and a set of tools both to generate and to check these proofs. Such a proof enables the equivalence to be established for individual executions of the compiler, even if the overall correctness of the compiler cannot be guaranteed. In prior work [6, 7], we devised a framework for certifying the results of standard knowledge compilation. This paper extends this framework and associated tools to handle projected knowledge compilation.

For standard knowledge compilation, the task is to prove that $\varphi (X)\equiv \psi (X)$, i.e., that the CNF and the d-DNNF representations are logically equivalent. In our framework, d-DNNF formulas are represented by directed acyclic graphs that we refer to as “partitioned-operation graphs” (POGs). These graphs have Boolean variables and their complements as terminal nodes, Boolean sum and product operations as nonterminal nodes, and edges from each operation to its arguments. The root node of the POG is denoted $𝐫$. In the CPOG (for “Certified POG”) framework, a proof consists of a sequence of equivalence-preserving clause addition and deletion steps.

The equivalence proof for standard knowledge compilation has two phases. The forward implication phase serves to prove $\varphi \Rightarrow \psi$, i.e., that any assignment satisfying the input formula also satisfies the compiled formula. It starts with the clauses for $\varphi$, along with clauses providing a Tseitin encoding of the compiled formula $\psi$, denoted $\theta (X,Z)$, where $Z$ is the set of auxiliary variables introduced by the encoding. The proof continues with a sequence of added clauses, each of which must satisfy the reverse unit propagation (RUP) property [25, 43] with respect to the existing clauses. This property guarantees that the added clause is logically implied by the earlier clauses. The forward implication phase terminates with the addition of a unit clause $[r]$, where $r$ is the variable in $Z$ denoting root node $𝐫$. Adding this clause proves that any assignment $\alpha$ that satisfies $\varphi$ must cause $\psi$ to evaluate to $1$. This phase can have exponential complexity. For example, when the input formula is unsatisfiable, the forward implication proof must be able to certify unsatisfiability.

The reverse implication phase for standard knowledge compilation serves to prove $\psi \Rightarrow \varphi$, completing the proof of equivalence. It does so by showing that each input clause satisfies the RUP property with respect to the combination of $\theta (X,Z)$ and unit clause $[r]$. That is, any assignment that falsifies the clause must cause $\psi$ to evaluate to $0$ (false). This clause can therefore be deleted without affecting the set of satisfying assignments. This portion of the proof is guaranteed to have polynomial complexity, since clausal entailment can be tested efficiently for d-DNNF formulas [9, 18].

For certifying projected knowledge compilation, we can build on the CPOG framework. The forward implication phase requires no change to the framework and only small changes to how the proofs are generated. Having the phase culminate with the addition of unit clause $[r]$ proves that any pair of assignments $\alpha$ to the data variables and $\beta$ to the quantified variables that satisfies input formula $\varphi$ will cause compiled formula $\psi$ to evaluate to $1$. This result holds even when $\psi$ contains only data variables and therefore depends only on assignment $\alpha$.

On the other hand, it is less clear how to generalize the reverse implication phase to handle projection. The input clauses contain both data and quantified variables, and so the simple strategy of showing that each individual input clause is implied by the compiled formula (containing only data variables) will not suffice. Instead, we handle the existential quantification via a form of Skolemization [3], associating some assignment $\beta$ to the quantified variables for each satisfying assignment $\alpha$ to the data variables. We do so by extending the POG representation to include Skolem nodes, representing partial assignments to the quantified variables. This “Skolem POG” then represents two d-DNNF formulas:

• $\mathrm{■}$

  Interpreting the Skolem nodes as tautologies gives the compiled representation $\psi (D)$. This version is used in the forward implication phase.

• $\mathrm{■}$

  By interpreting the Skolem nodes as Boolean products, the formula assigns values to both data and quantified variables. This makes it possible to deduce a Skolem assignment $\beta$ for any satisfying data assignment $\alpha$. This version serves as the basis for the input clause deletion steps in the reverse implication phase.

The Skolem POG can be generated by a combination of minor modifications to the projected knowledge compiler and postprocessing to partition the Boolean products into product and Skolem nodes.

In a prototype implementation of a proof generator and checker for projected model compilation, we found that storing the clausal representation of a Skolem POG, plus the proof steps for a RUP derivation of the input clauses in the reverse implication phase, led to excessive file sizes for the proofs – the degree for many of the Skolem nodes can be in the thousands and the size of each RUP step is linear in the size of the Skolem POG. To reduce file sizes and to speed up proof generation and checking, we shifted responsibility for proving that the input clauses can be deleted from the proof generator to the proof checker. As a result of this shift, we can also have the checker make inferences directly on the Skolem POG, rather than on its clausal representation. Since the test for each input clause has linear complexity (in the size of the Skolem POG), this shift in responsibility still fulfills a requirement for propositional proof systems that the proof must be checkable in polynomial time, with respect to the size of the proof [14].

This paper describes how our earlier work on certifying the results of a standard knowledge compiler can be extended to those of a projected knowledge compiler. It provides background on the relevant logical foundations, the extension of the POG representation to include Skolem nodes, the structure of both the forward and the reverse implication phases, and a sketch of a soundness proof for the framework. We also discuss the use of HOL4 and CakeML to formally verify the soundness proof and to implement a formally verified proof checker.

We present experimental results for our implementation, consisting of modified versions of D4 and our earlier proof generation and checking tools. By shifting the reverse implication phase of the proof to the proof checker, our framework scales to formulas having large d-DNNF representations.

In terms of prior research, there has been some work on proof frameworks for model counting [5, 12, 23], along with comparisons of the expressive power of the different frameworks [4]. In addition, another proof framework has been developed for standard knowledge compilation [10]. We know of no previous work extending any of these frameworks to handle projection. Indeed, the literature on projected model counting and projected knowledge compilation is very sparse. Several algorithms and tools for projected knowledge compilation and model counting have been published, based on top-down approaches [1, 27, 31, 32, 35, 39], decision diagrams [20], and dynamic programming [22], but none of these can certify their results.

We have found that formal proof assistants are essential in uncovering the many subtle details that can arise in devising a sound proof framework. Working with a proof assistant also let us explore possible optimizations in the proof framework and checker with complete confidence of their soundness. In this work, we shifted from Lean 4 [19] to the HOL4 proof assistant [40]. We did so in part to take advantage of the CakeML programming language [29], which has a formally verified compiler [42] and a large body of support for developing verified machine-code implementations of propositional proof frameworks [24, 41].

A Boolean formula $\varphi$ over one or more disjoint sets of variables $X_1,X_2,\mathrm{\dots },X_m$, is written as $\varphi (X_1,X_2,\mathrm{\dots },X_m)$ for clarity or as simply $\varphi$ when the context is clear.

The dependency set for Boolean formula $\varphi$, denoted $𝒱(\varphi )$, consists of all variables occurring in it. An assignment for a set of variables $X$ is a mapping $\alpha :X\to \{0,1\}$. When an assignment includes a value for every variable in $𝒱(\varphi )$, it is said to be total; otherwise it is partial. We assume assignments are total unless explicitly stated. The set of all total assignments for $X$ is denoted $𝒰(X)$. For formula $\varphi$ with dependency set $X$, its set of models, denoted $ℳ(\varphi )$ consists of all assignments in $𝒰(X)$ that satisfy the formula. For assignments $\alpha \in 𝒰(X)$ and $\beta \in 𝒰(Y)$, where $X\cap Y=\mathrm{\varnothing }$, we write $\alpha \cdot \beta$ as the assignment in $𝒰(X\cup Y)$ assigning $x$ to $\alpha (x)$ when $x\in X$ and to $\beta (x)$ when $x\in Y$. A literal is either a variable $x$ or its complement $\overline{x}$. The symbol $\mathrm{\ell }$ denotes a generic literal. Clauses are written as disjunctions, except that a unit clause, consisting of a single literal $\mathrm{\ell }$ is written as $[\mathrm{\ell }]$.

With a projected formula $\varphi (D,Y)$ the variables are partitioned into a set of data variables $D$ and a set of quantified variables $Y$. Its set of data models, denoted ${ℳ}_D(\varphi )$ is defined as

The task of projected knowledge compilation is to convert a CNF formula $\varphi (D,Y)$ into a formula $\psi (D)$ such that $ℳ(\psi )={ℳ}_D(\varphi )$. Furthermore, $\psi$ should be in a form for which computing important properties, such as the number of models, can be performed in polynomial time, relative to the size of $\psi$.

The class of Boolean formulas known as deterministic, decomposable, negation-normal form (d-DNNF) is defined recursively as formulas $\psi$ of the form:

Literals:

$x$ and $\overline{x}$ for Boolean variable $x$.

Decomposable Products [15, 18]:

${\psi }_1\wedge {\psi }_2\wedge \mathrm{\cdots }\wedge {\psi }_m$ where $𝒱({\psi }_i)\cap 𝒱({\psi }_j)=\mathrm{\varnothing }$ for

Deterministic Sums [16, 18]:

${\psi }_1\vee {\psi }_2\vee \mathrm{\cdots }\vee {\psi }_m$ where $ℳ({\psi }_i)\cap ℳ({\psi }_j)=\mathrm{\varnothing }$ for . Here we assume for all $1\le i\le m$, that $ℳ({\psi }_i)\subseteq 𝒰(X)$ for a common set of variables $X$.

We represent d-DNNF formulas as partitioned-operation graphs (POGs) [6, 7]. These are directed acyclic graphs where the terminal nodes represent literals and the nonterminal nodes represent product and sum operations. The root node is denoted $𝐫$.

As a running example throughout this paper, Figure 1 shows the declaration for a CNF formula encoding the disjunction of data variables $a$ and $b$, with quantified variables $x$ and $y$. Following the DIMACS CNF notation, literals are represented as integers. In this case, we number the variables $a$ and $b$ as 1 and 2 and the variables $x$ and $y$ as 3 and 4. The two comment lines (beginning with ‘c’) indicate that the file encodes a projected model counting problem with variables 1 ($a$) and 2 ($b$) as the data variables. With clause 1, when $a$ is assigned $0$, either $x$ or $y$ must be assigned $1$. With clauses 3 and 4, assigning $1$ to either $x$ or $y$ will force $b$ to be assigned $1$.

Given a CNF formula $\varphi (D,Y)$ and a d-DNNF formula $\psi (D)$, represented as a POG, we would like to generate a proof that $ℳ(\psi )={ℳ}_D(\varphi )$. We do so by converting $\psi$ into clausal form as a CNF formula $\theta (D,Z)$, where $Z$ is a set of extension variables used to encode the product and sum operations, according to a Tseitin encoding [38]. The root variable for the POG is defined as the extension variable $r$ associated with root node $𝐫$. This encoding has the property that for any $\alpha \in 𝒰(D)$, there is a unique assignment $\gamma \in 𝒰(Z)$ such $\alpha \cdot \gamma \in ℳ(\theta )$. We refer to this assignment as ${\gamma }_{\alpha }$. Furthermore, this assignment will satisfy ${\gamma }_{\alpha }(r)=1$ if and only if $\alpha \in ℳ(\psi )$. We use the notation ${\theta }_r(D,Z)$ to represent the formula $\theta (D,Z)\cup \{[r]\}$, the combination of the Tseitin encoding of the POG and a unit clause with the root literal requiring the POG to evaluate to $1$. Formula ${\theta }_r$ therefore serves as the clausal representation of d-DNNF formula $\psi$.

The proof of $ℳ(\psi )={ℳ}_D(\varphi )$ consists of two phases. The forward implication phase serves to prove that any data model $\alpha$ for $\varphi (D,Y)$ will be a model for $\psi (D)$. With ${\theta }_r(D,Z)$ serving as the clausal representation of $\psi$, we can write this as

We can transform this formula by bringing $\beta$ outward and inverting the sense of the quantification. Furthermore, we can make use of the fact that $\gamma$ is uniquely determined by $\alpha$. These changes yield the formula

We can see here that the assignments to both the data variables and the quantified variables are quantified in the same manner. We can therefore use the same method to generate and check this proof as is done with standard knowledge compilation [6, 7]. Starting with the combined clauses $\varphi (D,Y)$ and $\theta (D,Z)$, the proof of (3) consists of a sequence of clause addition steps leading to the addition of the unit clause $[r]$. In doing so the proof transforms $\theta$, the clausal representation of the POG operations, into ${\theta }_r$, the clausal representation of the d-DNNF formula $\psi$.

The reverse implication phase serves to prove that, for any assignment $\alpha$ satisfying $\psi (D)$, there is a $\beta \in 𝒰(Y)$ such that $\alpha \cdot \beta$ satisfies $\varphi (D,Y)$. Working directly with the d-DNNF formula $\psi$, we can write this as:

We can bring $\beta$ outward, yielding

Here, the quantifications of $\alpha$ and $\beta$ differ: they require the implication to hold for all data assignments $\alpha$ but for only some quantified assignment $\beta$ for a given $\alpha$ – and even then only when $\alpha$ is a data model of $\psi$. The task of generating such an assignment is known as Skolemization, and $\beta$ is referred to as a Skolem assignment for $\alpha$ [2, 3].

A Skolem POG is an extension of the POG representation that serves two roles:

Compiler Output:

It provides the POG representation of a d-DNNF formula $\psi (D)$ forming the output of a projected knowledge compiler.

Skolemization:

It augments this representation with a method for computing a Skolem assignment $\beta$ for any assignment $\alpha \in ℳ(\psi )$ such that $\alpha \cdot \beta \in ℳ(\varphi )$.

Generating the Skolem POG and the forward implication proofs involves only modest changes to the knowledge compiler and to the proof generator. A more substantial change is required for the shift of the reverse implication phase to the proof checker.

We have formally verified the soundness of our proof framework in HOL4 and developed a verified proof checker using CakeML. Here, we provide an informal justification of the proof framework to give some intuition for its soundness. Section 8.2 provides more details on the formally verified checker.

We implemented a proof generator in C++, along with two proof checkers: one written in C, and the other in CakeML and verified with HOL4. The C checker uses multithreading when performing the reverse-implication check, taking advantage of the property that the input clause deletion checks can be performed independently.

All experiments were run on a 2021 Apple MacBook Pro, with a 3.2 Ghz Apple M1 8-core processor and 64 GB of RAM. All reported times are for elapsed (“wall-clock”) times.

For benchmark problems, we used the private and public formulas from the 2024 unweighted and weighted projected model counting competitions.⁵⁵5Available at https://zenodo.org/records/14249068. There were 200 formulas for each track, but with some duplicates across the two tracks, yielding a set of 389 unique benchmark formulas.

We ran two versions of D4 on the 389 benchmark formulas: an unmodified version generating just the d-DNNF data, and the modified version that included the information from which the Skolem POG could be constructed. Both successfully compiled 175 formulas within the time limit of 1,000 seconds. The modified version of D4 ran fast enough: at most $1.8\times$ slower than the unmodified version, with a median of $1.11\times$.

Figure 5 documents an important feature of the 175 compiled benchmark formulas, showing the number of data variables (Y-axis), compared to the total number of variables (X-axis). For many formulas, the data variables constitute only a small fraction of the total. For one, only 100 of its 906,806 ($0.0001\%$) variables are data variables. The median ratio of data variables to total variables is $2.0\%$. This property has significant impact on the sizes of the Skolem POGs and the challenge of checking reverse implication. The color coding of the data in the plots of Figure 5 and 6 gives a preview of our success in verifying these benchmarks: 172 of them (green) completed the full verification. For the remaining 3 (red), the proof generator timed out, with a time limit of 10,000 seconds.

We generated the Skolem POGs from the output of the modified version of D4, and we could also determine how large the POG would be without the Skolem information, as illustrated on the Y and X axes of Figure 6, respectively. We measure POG sizes in terms of the number of clauses in their Tseitin encodings. This is also equal to the number of nodes plus the number of edges in the graphs. As can be seen, the Skolem POGs tend to me much larger than the regular POGs, with size ratios ranging up to $4857\times$ with a median of $34\times$. Considering the large fraction of quantified variables in these formulas, these large size ratios are to be expected.

Figure 7 compares the runtime for verification versus for compilation for the 172 formulas that were fully verified. The X axis shows the time to run the modified version of D4, while the Y axis shows the time to postprocess the D4 output, generate and check the proof, and compute an unweighted or weighted model count. The reverse-implication check uses 7-way multithreading. For 19 formulas, compilation took longer than verification, while it required less for the others. At worst, verification required $191.7\times$ longer, with a median of $2.95\times$.

Our use of multithreading provides a significant benefit. Verifying all 172 benchmarks requires a total of $20.8$ hours with the multithreaded version and $37.9$ hours with a sequential version. This includes proof generation, forward and reverse checking, and model counting. Parallelism is only used when performing the reverse-implication check on the input clauses. This portion requires $8.4$ hours with multithreading and $25.5$ hours sequentially, a speedup of $3.0\times$. This is a reasonable performance gain for a memory-intensive application. Multithreading also reduces the benchmark with the longest sequential verification time from $15.3$ to $4.4$ hours.

We ran the formally verified checker on the 172 formulas for which the proof generator completed. It verified 156 of them, and it exceeded its heap memory limit of 48 GB for the remaining 16. Comparing its performance to the unverified checker for the 156 completed checks, it ran between $2.9\times$ faster and $17.7\times$ slower, with a median of $1.5\times$ slower. This is remarkable performance for a formally verified tool.

Overall, our tool handled these formulas well. On the other hand, we found that letting D4 run for longer than 1000 seconds leads to d-DNNF formulas that are beyond the capacity of our current tool chain. The major weakness is in generating forward implication proofs.

We have shown that the output of a projected knowledge compiler can be certified by extending our prior proof framework for standard knowledge compilation. The compiler already has access to information about how the quantified variables can be assigned according to the assignment to the data variables. By having it provide this information and then postprocessing the output, the proof generator can construct a Skolem POG, serving the dual roles of encoding the projected formula and the Skolem assignments. Certification proceeds by proving implication in both directions, within forward implication proved by clausal additions and reverse implication checked directly on the generated formula.

We were able to formally verify the soundness of our proof framework in HOL4 and develop a formally verified checker. A successful run of the checker gives full confidence that the compiled formula $\psi (D)$ has the same data models as the input formula $\theta (D,Y)$. In our earlier effort to devise a proof framework for standard knowledge compilation, the formal verification effort uncovered some subtle requirements that we had overlooked. Our experience was quite different this time. We correctly anticipated the requirements to achieve soundness. On the other hand, having the support of formal verification enabled us to be more aggressive in exploring refinements to improve the combined proof generator and checker performance. These optimizations greatly improved the scaling of our tools.

Projected knowledge compilation, and the closely related topic of projected model counting, are active areas of research, with many optimizations being discovered. Our framework will only be of value if it can keep up with these innovations. We describe two examples here.

First, some have discovered conditions under which it is possible for the compiler or model counter to split on quantified variables, remove the literals for these variable in the compiled output, and still have the result be a d-DNNF formula [27]. This requires more extensive mutual exclusion proofs for the sum operations than the simple cases illustrated in the SCPOG example of Figure 4. Our framework, described in Appendix A, includes support for such proofs. For a sum node with children represented by literals ${\mathrm{\ell }}_1$ and ${\mathrm{\ell }}_2$, the mutual exclusion proof can be generated with a proof-generating SAT solver that includes clauses encoding the two branches, plus the unit literals $[{\mathrm{\ell }}_1]$ and $[{\mathrm{\ell }}_2]$. The proof clauses in the UNSAT proof are augmented by the literals ${\overline{\mathrm{\ell }}}_1$ and ${\overline{\mathrm{\ell }}}_2$, and so the empty clause of the proof becomes the mutual exclusion ${\overline{\mathrm{\ell }}}_1\vee {\overline{\mathrm{\ell }}}_2$.

Second, some have discovered cases where input clauses can be removed via blocked-clause elimination [32]. Significantly, they do so as an inprocessing step, where the conditions for the elimination hold only under a partial assignment to the variables. Our framework can handle the special case of pure-literal elimination, where the blocked clause has been reduced to a unit literal, by having the knowledge compiler record the literal as being satisfied. Handling more general cases would seem to require a new way to prove reverse implication for those input clauses that have been eliminated.