Pith. sign in

REVIEW 5 minor 1 cited by

Certified Knowledge Compilation with Application to Formally Verified Model Counting

T0 review · 0 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A checkable proof format lets a formally verified checker certify that a knowledge compiler's output represents the original formula.

desk verdict First formally verified model-counting toolchain with a machine-checked soundness theorem; the trust boundary is real but disclosed, and the paper deserves serious peer review. read the letter →

arxiv 2501.12906 v1 pith:4RVA4ZHF submitted 2025-01-22 cs.LO

Randal E. Bryant , Wojciech Nawrocki , Jeremy Avigad , Marijn J. H. Heule This is my paper · ORCID
classification cs.LO
keywords modelcountingknowledgecompilationformalverificationdecision-DNNFPartitioned-OperationGraphsCPOGextendedresolutionproofchecking
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Model counting is intractable for general Boolean formulas, so practical tools first compile the formula into decision-DNNF, a structured form that supports fast counting; but until now the compiler's output carried no certificate that it represents the same formula. This paper introduces Partitioned-Operation Graphs (POGs), a general form that subsumes the representations knowledge compilers produce, together with CPOG, a clausal proof format proving that a POG is equivalent to an input CNF formula. The paper implements a proof generator that turns D4's decision-DNNF output into such proofs, and a proof checker and ring evaluator formally verified in a machine-checked proof assistant. The main theorem states that whenever the verified checker finishes successfully, the input formula and the POG root are logically equivalent, so the computed weighted or unweighted model count is correct. If this holds, it gives the first end-to-end formally verified toolchain for model counting.

What carries the argument

The central object is the Partitioned-Operation Graph (POG), a directed acyclic graph whose product nodes require disjoint child dependency sets and whose sum nodes require pairwise disjoint child model sets, so that ring evaluation reduces to one bottom-up traversal. The proof machinery is CPOG, an extended-resolution clausal proof system: each POG node is introduced by Tseitin-style defining clauses, clause additions and deletions are justified by reverse unit propagation (RUP), and a successful proof ends with only the root unit clause plus the defining clauses active. The formal proof development proves that the checker's invariants imply soundness; the effort also exposed a subtle necessary condition, namely that the mutual-exclusion hint for a sum node may reference only defining clauses, not arbitrary input clauses.

What would settle it

Take small random CNF formulas, certify them with the toolchain, and compare the checker's unweighted count with exhaustive enumeration over all assignments; any mismatch would refute the equivalence and counting claim. A more targeted test is to mutate a valid CPOG file, such as deleting one input-clause deletion step or weakening a sum-node hint, and confirm that the verified checker rejects it; acceptance would indicate a flaw in the invariants or in code extraction.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1: if the proof checker has assembled POG $P$ with root node $r$ starting from input formula $\varphi_I$, and the final conditions of Section 7.2 hold, then $\varphi_I$ is logically equivalent to $\varphi_r$. The equivalence is maintained step by step: every clause addition and deletion preserves the set of satisfying assignments over the input variables, and the defining clauses for POG nodes give each node a unique value under every total input assignment. The paper reports that this supplies the first formally verified toolchain for weighted and unweighted model counting, with experiments certifying all but the largest decision-DNNF graphs produced by D4 on 2022 model-counting competition benchmarks.

Load-bearing premise

The executed toolchain additionally assumes that the proof-assistant kernel is sound, that extracted array and arbitrary-precision arithmetic code behaves as specified, and that the parser reads input files correctly; the last point is mitigated only by reprinting the parsed formula and proof and asking a human to diff them.

Editorial extensions

If this is right

  • Knowledge compiler outputs become auditable: the toolchain produces and verifies full equivalence proofs for 111 of 123 benchmark formulas, plus one-sided proofs for another seven.
  • Verification is end-to-end with respect to the original input, so a logically equivalent preprocessed formula is certified together with the preprocessing and compilation steps.
  • The formally verified checker has similar scaling to the optimized prototype, running within about a factor of four for all but the smallest inputs.
  • Weighted and unweighted model counts are produced by verified ring evaluation; reported outputs include a count with 260,909 decimal digits.
  • The proof framework is not tied to any particular compiler algorithm and is designed to extend to arbitrary POGs and semiring queries.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial: the guarantee is conditional on trust in the proof-assistant kernel, code extraction for arrays and arbitrary-precision arithmetic, and the parser; the printed-and-diffed parser check is a human step, so an unattended run inherits those assumptions.
  • Editorial: CPOG could become the standard interchange format for certified knowledge compilation, much as DRAT became standard for unsatisfiability proofs, giving compiler developers a uniform way to catch regressions.
  • Editorial: because formal verification surfaced a hidden soundness bug in the sum-node hint restriction, other knowledge-compilation proof frameworks that rest on informal soundness arguments are candidates for similar re-examination.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

0 major / 5 minor

Summary. This paper introduces Partitioned-Operation Graphs (POGs), a graph-based normal form for Boolean formulas with decomposable products and deterministic sums, and CPOG, a clausal proof format that certifies the logical equivalence of a CNF formula and a POG. The authors implement a proof generator that converts decision-DNNF graphs produced by the D4 knowledge compiler into CPOG proofs, and they develop a proof checker and ring evaluator in Lean 4, formally verifying that a successfully checked CPOG file yields a POG equivalent to the input formula (Theorem 1, Section 10) and that ring evaluation on the POG gives the correct weighted or unweighted model count. Experiments on 123 benchmarks from the 2022 model counting competition show full verification for 111 of them, with one-sided proofs for 7 and no validation for 5, and the verified checker is within 4x of the prototype on the reduced benchmark set.

Significance. The paper's main contribution is the first certification framework for knowledge compilation whose soundness theorem is machine-checked, together with a practical generator and checker. The formalization covers the core invariants (partitioning, unique extension of assignments, equivalence over input variables), ring evaluation equality, and a model-counting theorem, and it also led to the discovery of a subtle soundness condition for the partitioned-sum rule and an exploitable weakness in the CD4 framework. The artifact (Lean 4 development and C/C++ generator) is publicly available, and the experiments are thorough, including ablation of the lemma and literal-grouping optimizations. The main limitation is the disclosed trust boundary: the parser and code extraction are not formally verified, and the checker's theorem is stated for the in-memory representation built by the unverified parser. This is standard for verified clausal proof checkers and is mitigated by --print-cnf/--print-cpog diffing, so it does not undermine the mathematical result.

minor comments (5)
  1. [Abstract / Section 10] The abstract describes the system as 'the first formally verified toolchain for weighted and unweighted model counting', but Section 10 (Trust) explicitly states that the parser is not verified and that code extraction for arrays and arbitrary-precision arithmetic is trusted. To make the claim match the verified scope, I suggest rephrasing the abstract to something like 'the first toolchain with a formally verified proof checker and model counter' or 'the first certification framework whose proof system and checker are machine-checked'.
  2. [Section 5, last paragraph] The sentence 'As is described in 10, we have proved these three equations using Lean 4' should read 'As is described in Section 10, ...' – the section reference is missing the word 'Section'.
  3. [Section 13.2] In the smoothing construction, the formula replacing phi_i is printed as '( x∨p x)∧p phi_i'; this should be '(x ∨p ¬x) ∧p phi_i' (or a similar tautology that introduces x), otherwise the replacement does not add x to the dependency set. Please correct the typo.
  4. [Section 12.2] The hybrid rule (tree ratio ≤ 5.0 and tree-size thresholds) was selected using the same reduced benchmark set on which Figures 4 and 5 report performance. The paper notes the data were too sparse for more tuning, but it would be good to explicitly acknowledge that the subsequent performance numbers for the hybrid approach on the full benchmark set may therefore be somewhat optimistic, since the threshold is partially fit to a subset of those benchmarks.
  5. [Section 12.6] The sentence reporting that the verified checker runs 'between 3.42× faster and 4.39× slower' than the prototype is surprising for a Lean-extracted program; consider adding a brief explanation of the outlier (e.g., startup effects or different data structures) so readers are not misled.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the formal derivation is self-contained and machine-checked, with only an explicitly disclosed trust boundary.

full rationale

The paper's central claim, Theorem 1, asserts that if the Lean-verified checker processes a CPOG proof and satisfies the final conditions, then the input CNF formula is logically equivalent to the assembled POG. The proof is a formal Lean derivation from the checker invariants, with the hard work being the maintenance of those invariants across each CPOG clause-addition, deletion, and node-declaration step. The ring-evaluation claim is likewise backed by the formal theorem ringEval_eq_weightSum, and the model-counting claim by countModels_eq_card_models; these are proved results, not definitions or renamed inputs. No parameter is fitted to data and then reported as a prediction: the hybrid proof-generation threshold is an engineering choice affecting runtime and proof size only, not the equivalence theorem or counting result. The paper explicitly discloses the unverified parser, code extraction of arrays and arbitrary-precision arithmetic, and reliance on the Lean kernel soundness; these are standard trust assumptions for verified checkers and are not circular. The self-reference to the authors' earlier SAT 2023 paper is merely a statement that this is an extended version and is not load-bearing. No circular step can be quoted from the equations or invariants that reduces Theorem 1 or the counting guarantee to its own assumptions.

Assumptions & free parameters 3 free parameters · 5 assumptions · 0 invented entities

The central soundness proof is machine-checked, so the remaining axioms are the standard trust assumptions for verified software: the Lean kernel, code extraction, and the unverified parser. The only numbers fitted to data are performance thresholds in the proof generator; they do not enter the equivalence proof or the counting theorem.

free parameters (3)
  • Hybrid proof generation tree-ratio threshold = 5.0
    Selected from 90 reduced benchmarks to choose monolithic versus structural forward proof generation; affects runtime and proof size, not the soundness claim (Section 12.2).
  • Monolithic shift tree-size threshold = 10^6
    The hybrid generator switches from structural to monolithic generation when tree size drops below this value; empirically tuned in Section 12.2 and performance-only.
  • Reduced benchmark set cutoffs = D4 time <= 1000 s, POG size <= 10^7 defining clauses
    Methodological choice to create a tractable evaluation set; does not alter the correctness result (Section 12.1).
assumptions (5)
  • domain assumption Soundness of the Lean 4 kernel and type theory
    Section 10 'Trust' explicitly lists trust in Lean's foundation and kernel checker as an assumption.
  • domain assumption Code extraction preserves semantics for efficient arrays and arbitrary-precision arithmetic
    Section 10 states that Lean code extraction replaces list-based arrays and natural/integer arithmetic with unverified efficient versions.
  • domain assumption Parser reads CNF and CPOG files faithfully; print/diff detects any parse error
    Parsing is not verified; the checker exposes --print-cnf and --print-cpog for human comparison (Section 10).
  • standard math Classical propositional logic and commutative ring axioms
    The formal model in Sections 3 and 10 is built on these standard mathematical foundations.
  • domain assumption RUP is a sound rule for clause addition and deletion
    The CPOG checker uses reverse unit propagation as the core implication-redundancy rule; soundness is proved in Lean for the stated rules.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Certified Knowledge Compilation with Application to Formally Verified Model Counting." pith.science (2026). https://pith.science/paper/4RVA4ZHF

@misc{pith2026250112906,
  author       = {Pith},
  title        = {Pith review of: Certified Knowledge Compilation with Application to Formally Verified Model Counting},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4RVA4ZHF}},
  note         = {Machine review of arXiv:2501.12906}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2501.12906 by the authors.

Figure 1
Figure 1. Certifying toolchain. The ring evaluator produces a weight [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Example formula (A), its POG representation (B), and its C [PITH_FULL_IMAGE:figures/full_fig_p012_2.png] view at source ↗
Figure 3
Figure 3. Example of lemma definition, proof, and application [PITH_FULL_IMAGE:figures/full_fig_p018_3.png] view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: Structural (Y axis) versus monolithic (X axis) forward imp [PITH_FULL_IMAGE:figures/full_fig_p025_4.png]
Figure 5
Figure 5. Figure 5: Structural (Y axis) versus monolithic (X axis) proof sizes [PITH_FULL_IMAGE:figures/full_fig_p026_5.png]
Figure 6
Figure 6. Figure 6: Combined runtime for CPOG proof generation, checking, a [PITH_FULL_IMAGE:figures/full_fig_p028_6.png]
Figure 7
Figure 7. Figure 7: Total number of clauses in CPOG file as function of number o [PITH_FULL_IMAGE:figures/full_fig_p029_7.png]
Figure 8
Figure 8. Figure 8: Proof clauses when one or both optimizations is enabled, ve [PITH_FULL_IMAGE:figures/full_fig_p031_8.png]
Figure 9
Figure 9. Figure 9: Times for Verified Checker versus Prototype Checker. B [PITH_FULL_IMAGE:figures/full_fig_p032_9.png]
Figure 10
Figure 10. Figure 10: Times for CD4 Toolchain versus CPOG Toolchain. Times includ [PITH_FULL_IMAGE:figures/full_fig_p034_10.png]
Figure 11
Figure 11. Figure 11: Running Time for MICE versus our proof chains. Times inclu [PITH_FULL_IMAGE:figures/full_fig_p035_11.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. A Distributed Framework for Compiling and Reasoning with d-DNNF

    cs.DC 2026-07 conditional novelty 6.0 of 10

    A Cube-and-Conquer framework compiles CNF formulas into a virtual d-DNNF distributed across workers, enabling counting, direct access, and uniform sampling under conditioning.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages · cited by 1 Pith paper

  1. [1]

    Beame, J

    P. Beame, J. Li, S. Roy, and D. Suciu. Lower bounds for exac t model counting and applications in probabilistic databases. In Uncertainty in Artificial Intelligence , pages 52–61, 2013

    work page 2013

  2. [2]

    M. Blum, A. K. Chandra, and M. N. Wegman. Equivalence of fr ee Boolean graphs can be decided probabilistically in polynomial time. Information Processing Letters, 10(2):80–82, 18 March 1980

    work page 1980

  3. [3]

    R. E. Bryant, W. Nawrocki, J. Avigad, and M. J. H. Heule. Ce rtified knowledge compilation with application to verified model counting. In Theory and Applications of Satisfiability Testing (SAT) . Schloss Dagstuhl, July 2023

    work page 2023

  4. [4]

    F. Capelli. Knowledge compilation languages as proof sy stems. In Theory and Applications of Satisfiability Testing (SAT) , volume 11628 of LNCS, pages 90–91, 2019

    work page 2019

  5. [5]

    Capelli, J.-M

    F. Capelli, J.-M. Lagniez, and P. Marquis. Certifying to p-down decision-DNNF compilers. In AAAI Conference on Artificial Intelligence (AAAI) , 2021. 37 Certified Knowledge Compilation Bryant, Nawrocki, Avigad, and Heule

    work page 2021

  6. [6]

    Cruz-Filipe, M

    L. Cruz-Filipe, M. J. H. Heule, W. A. Hunt, M. Kaufmann, an d P. Schneider-Kamp. Efficient certified RAT verification. In Conference on Automated Deduction (CADE) , volume 10395 of LNCS, pages 220–236, 2017

    work page 2017

  7. [7]

    Darwiche

    A. Darwiche. Demposable negation normal form. Journal of the ACM , 48, 2001

    work page 2001

  8. [8]

    Darwiche

    A. Darwiche. A compiler for deterministic, decomposabl e negation normal form. In Association for the Advancement of Artificial Intelligence (AAAI) , 2002

    work page 2002

Show all 38 references
  1. [9]

    Darwiche

    A. Darwiche. SDD: A new canonical representation of prop ositional knowledge bases. In Interna- tional Joint Conference on Artificial Intelligence , pages 819–826, 2011

    2011

  2. [10]

    Darwiche and P

    A. Darwiche and P. Marquis. A knowledge compilation map . Journal of Artificial Intelligence Research, 17, 2002

    2002

  3. [11]

    de Moura and S

    L. de Moura and S. Ulrich. The Lean 4 theorem prover and pr ogramming language. In Conference on Automated Deduction (CADE) , volume 12699 of LNAI, pages 625–635, 2021

    2021

  4. [12]

    J. K. Fichte, M. Hecher, and V. Roland. Proofs for propos itional model counting. In Theory and Applications of Satisfiability Testing (SAT) . Schloss Dagstuhl-Leibniz-Zentrum f¨ ur Informatik, 2022

    2022

  5. [13]

    E. I. Goldberg and Y. Novikov. Verification of proofs of u nsatisfiability for CNF formulas. In Design, Automation and Test in Europe (DATE) , pages 886–891, 2003

    2003

  6. [14]

    M. J. H. Heule, W. A. Hunt, M. Kaufmann, and N. D. Wetzler. Efficient, verified checking of propositional proofs. In Interactive Theorem Proving , volume 10499 of LNCS, pages 269–284, 2017

    2017

  7. [15]

    M. J. H. Heule, W. A. Hunt Jr., and N. D. Wetzler. Trimming while checking clausal proofs. In Formal Methods in Computer-Aided Design (FMCAD) , pages 181–188, 2013

    2013

  8. [16]

    M. J. H. Heule, W. A. Hunt, Jr., and N. D. Wetzler. Verifyi ng refutations with extended resolution. In Conference on Automated Deduction (CADE) , volume 7898 of LNCS, pages 345–359, 2013

    2013

  9. [17]

    M. J. H. Heule, M. Seidl, and A. Biere. A unified proof syst em for QBF preprocessing. In International Joint Conference on Automated Reasoning (IJ CAR), volume 8562 of LNCS, pages 91–106, 2014

    2014

  10. [18]

    Huang and A

    J. Huang and A. Darwiche. The language of search. Journal of Artificial Intelligence Research , 22:191–219, 2007

    2007

  11. [19]

    J¨ arvisalo, M

    M. J¨ arvisalo, M. J. H. Heule, and A. Biere. Inprocessin g rules. In International Joint Conference on Automated Reasoning (IJCAR) , volume 7364 of LNCS, pages 355–370, 2012

    2012

  12. [20]

    Kimmig, G

    A. Kimmig, G. V. den Broeck, and L. D. Raedt. Algebraic mo del counting. Journal of Applied Logic, 22:46–62, July 2017

    2017

  13. [21]

    Lagniez and P

    J.-M. Lagniez and P. Marquis. An improved decision-DNN F compiler. In International Joint Conference on Artificial Intelligence , pages 667–673, 2017

    2017

  14. [22]

    Lagniez and P

    J.-M. Lagniez and P. Marquis. Preprocessing for propos itional model counting. In AAAI Confer- ence on Artificial Intelligence (AAAI) , 2021

    2021

  15. [23]

    P. Lammich. Efficient verified (UN)SAT certificate checki ng. J. Autom. Reason. , 64(3):513–532, 2020

    2020

  16. [24]

    Limperg and A

    J. Limperg and A. H. From. Aesop: White-box best-first pr oof search for Lean. In Certified Programs and Proofs (CPP) , pages 253–266. ACM, 2023

    2023

  17. [25]

    Monet and D

    M. Monet and D. Olteanu. Towards deterministic decompo sable circuits for safe queries. In Alberto Mendelzon International Workshop on Foundations of Data Ma nagement (AMW) , 2018

    2018

  18. [26]

    Muise, S

    C. Muise, S. A. McIlraith, and J. C. Beck. Dsharp: Fast d- DNNF compilation with sharpSAT. In Canadian Conference on Artificial Intelligence , 2012

    2012

  19. [27]

    Nipkow, L

    T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL. A proof assistant for higher-order logic , volume 2283 of Lecture Notes in Computer Science . Springer Verlag, Berlin, 2002

    2002

  20. [28]

    Pollitt, M

    F. Pollitt, M. Fleury, and A. Biere. Faster LRAT checkin g than solving with CaDiCaL. In Theory and Applications of Satisfiability Testing (SAT) . Schloss Dagstuhl, July 2023. 38 Certified Knowledge Compilation Bryant, Nawrocki, Avigad, and Heule

    2023

  21. [29]

    J. A. Robinson. A machine-oriented logic based on the re solution principle. J.ACM, 12(1):23–41, January 1965

    1965

  22. [30]

    A. Shih, G. Van den Broeck, P. Beame, and A. Amarilli. Smo othing structured decomposable circuits. In Advances in Neural Information Processing Systems , volume 32, 2019

    2019

  23. [31]

    Y. K. Tan, M. J. H. Heule, and M. O. Myreen. cake lpr: Verified propagation redundancy checking in CakeML. In Tools and Algorithms for the Construction and Analysis of Sy stems (TACAS), Part II, volume 12652 of LNCS, pages 223–241, 2021

    2021

  24. [32]

    The Coq proof assistant, 2024

    The Coq development team. The Coq proof assistant, 2024 . https://coq.inria.fr/

    2024

  25. [33]

    G. S. Tseitin. On the complexity of derivation in propos itional calculus. In Automation of Rea- soning: 2: Classical Papers on Computational Logic 1967–19 70, pages 466–483. Springer, 1983

    1967

  26. [34]

    Ullrich and L

    S. Ullrich and L. de Moura. Counting immutable beans: re ference counting optimized for purely functional programming. In Implementation and Application of Functional Languages (I FL), pages 3:1–3:12. ACM, 2019

    2019

  27. [35]

    L. G. Valiant. The complexity of enumeration and reliab ility problems. SIAM Journal of Com- puting, 8(3):410–421, 1979

    1979

  28. [36]

    Van Gelder

    A. Van Gelder. Verifying RUP proofs of propositional un satisfiability. In Proc. of the 10th Int. Symposium on Artificial Intelligence and Mathematics (ISAIM 2008 ), 2008

    2008

  29. [37]

    N. D. Wetzler, M. J. H. Heule, and W. A. Hunt Jr. DRAT-trim : Efficient checking and trimming using expressive clausal proofs. In Theory and Applications of Satisfiability Testing (SAT) , volume 8561 of LNCS, pages 422–429, 2014

    2014

  30. [38]

    Zhang and S

    L. Zhang and S. Malik. Validating SAT solvers using an in dependent resolution-based checker: Practical implementations and other applications. In Design, Automation and Test in Europe (DATE), pages 880–885, 2003. 39

    2003

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.