Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Certified Knowledge Compilation with Application to Formally Verified Model Counting

Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule

TL;DR

This work addresses the trust problem in knowledge compilation for model counting by introducing Partitioned-Operation Graphs (POGs) and the certifiable CPOG framework, enabling proofs of logical equivalence between CNF inputs and compiled representations. A two-pronged proof strategy—forward (to show input models imply the POG root) and reverse (to show POG root implies input models)—is supported by a formally verified Lean 4 implementation of the proof checker and ring evaluator, forming the first fully verified toolchain for weighted and unweighted model counting. The authors demonstrate end-to-end verification on benchmarks from recent model-counting competitions, analyze optimizations (lemmas, literal grouping), and compare performance to CD4 and MICE, showing favorable robustness and scalability in many but not all cases. The work lays a rigorous foundation for trusted knowledge compilation and model counting, with clear paths to extend to arbitrary POGs and semiring evaluations, thus broadening its applicability in verification and AI contexts.

Abstract

Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when formulas are expressed in a special form, such as the decision decomposable negation normal form (decision-DNNF). Knowledge compilation is the process of converting a formula into such a form. Unfortunately existing knowledge compilers provide no guarantee that their output correctly represents the original formula, and therefore they cannot validate a model count, or any other computed value. We present Partitioned-Operation Graphs (POGs), a form that can encode all of the representations used by existing knowledge compilers. We have designed CPOG, a framework that can express proofs of equivalence between a POG and a Boolean formula in conjunctive normal form (CNF). We have developed a program that generates POG representations from the decision-DNNF graphs produced by the state-of-the-art knowledge compiler D4, as well as checkable CPOG proofs certifying that the output POGs are equivalent to the input CNF formulas. Our toolchain for generating and verifying POGs scales to all but the largest graphs produced by D4 for formulas from a recent model counting competition. Additionally, we have developed a formally verified CPOG checker and model counter for POGs in the Lean 4 proof assistant. In doing so, we proved the soundness of our proof framework. These programs comprise the first formally verified toolchain for weighted and unweighted model counting.

Certified Knowledge Compilation with Application to Formally Verified Model Counting

TL;DR

This work addresses the trust problem in knowledge compilation for model counting by introducing Partitioned-Operation Graphs (POGs) and the certifiable CPOG framework, enabling proofs of logical equivalence between CNF inputs and compiled representations. A two-pronged proof strategy—forward (to show input models imply the POG root) and reverse (to show POG root implies input models)—is supported by a formally verified Lean 4 implementation of the proof checker and ring evaluator, forming the first fully verified toolchain for weighted and unweighted model counting. The authors demonstrate end-to-end verification on benchmarks from recent model-counting competitions, analyze optimizations (lemmas, literal grouping), and compare performance to CD4 and MICE, showing favorable robustness and scalability in many but not all cases. The work lays a rigorous foundation for trusted knowledge compilation and model counting, with clear paths to extend to arbitrary POGs and semiring evaluations, thus broadening its applicability in verification and AI contexts.

Abstract

Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when formulas are expressed in a special form, such as the decision decomposable negation normal form (decision-DNNF). Knowledge compilation is the process of converting a formula into such a form. Unfortunately existing knowledge compilers provide no guarantee that their output correctly represents the original formula, and therefore they cannot validate a model count, or any other computed value. We present Partitioned-Operation Graphs (POGs), a form that can encode all of the representations used by existing knowledge compilers. We have designed CPOG, a framework that can express proofs of equivalence between a POG and a Boolean formula in conjunctive normal form (CNF). We have developed a program that generates POG representations from the decision-DNNF graphs produced by the state-of-the-art knowledge compiler D4, as well as checkable CPOG proofs certifying that the output POGs are equivalent to the input CNF formulas. Our toolchain for generating and verifying POGs scales to all but the largest graphs produced by D4 for formulas from a recent model counting competition. Additionally, we have developed a formally verified CPOG checker and model counter for POGs in the Lean 4 proof assistant. In doing so, we proved the soundness of our proof framework. These programs comprise the first formally verified toolchain for weighted and unweighted model counting.
Paper Structure (39 sections, 2 theorems, 3 equations, 11 figures, 2 tables)

This paper contains 39 sections, 2 theorems, 3 equations, 11 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Logical Foundations
  4. Ring Evaluation of a Boolean Formula
  5. Partitioned-Operation Graphs (POGs)
  6. Clausal Proof Framework
  7. The CPOG Representation and Proof System
  8. Syntax
  9. Semantics
  10. CPOG Example
  11. Node Declarations
  12. Forward Implication Proof
  13. Reverse Implication Proof
  14. Generating CPOG from decision-DNNF
  15. Forward Implication Proof
  16. ...and 24 more sections

Key Result

Proposition 1

Ring evaluation with operations $\neg$, $\mathbin{\land^\textsf{p}}$, and $\mathbin{\lor^\textsf{p}}$ satisfies the following for any weight function $w$:

Figures (11)

  • Figure 1: Certifying toolchain. The ring evaluator produces a weighted or unweighted count. Certification by the proof checker guarantees its correctness.
  • Figure 2: Example formula (A), its POG representation (B), and its CPOG proof (C), (E), and (F). The defining clauses (D) are implicitly defined by the POG declaration (C).
  • Figure 3: Example of lemma definition, proof, and application
  • Figure 4: Structural (Y axis) versus monolithic (X axis) forward implication proof generation times. The structural approach generally performed better for formulas with high tree ratios.
  • Figure 5: Structural (Y axis) versus monolithic (X axis) proof sizes. The monolithic approach generated shorter proofs in most cases.
  • ...and 6 more figures

Theorems & Definitions (7)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4: Ring Evaluation Problem
  • Proposition 1
  • Theorem 1
  • proof