Model Counting as a Sum of Products: Verified Translation and Variable Elimination in Lean 4
Abstract
Weighted model counting is the sum, over all assignments of the variables, of a product of clause indicators and literal weights, that is, an einsum over Boolean indices. Tensor-network and project-join model counters build on this view, but the translation from a formula to a sum of products, and the elimination of variables that makes it efficient, are normally trusted. We formalize both in Lean 4, using only its core library, and prove three results. First, the plan of a weighted CNF evaluates to its weighted model count, which is defined independently by enumerating all 2^n assignments. Second, bucket elimination along any order of the variables computes the same count. Third, an eliminated (nested) plan can be flattened to a sum of monomials by a verified compiler that draws bound names from a counter, so that no variable is captured, also when names are reused; composed, these give an end-to-end theorem. The development is executable; on small instances the choice of order changes the number of table entries by up to a factor of six. We make no performance claim against solvers.
The record contains the manuscript (LaTeX sources in the format of the Journal on Satisfiability, Boolean Modeling and Computation, and PDF) and the Lean 4 artifact (tic_sat_lean.zip), which builds with "bash build.sh" using Lean 4.35.0.
Related
- Quantum-Bridge: Verified lossless circuit translation between Qiskit and PennyLane with dependency-free zero-noise extrapolation
- Compiling index notation to sums of products: a verified functional pearl
- Accelerating Fourier--Motzkin elimination: redundancy removal and the choice of variable elimination order
- Clinical Scores and Machine Learning at Matched Variable Domains in Acute Appendicitis: Performance of Recommended Rule-Out Thresholds in a CT-Verified Cohort
- From Agro-Food By-Products to Precision Nutraceuticals: Bioactive Compounds, Molecular Mechanisms, Bioavailability and Clinical Translation
BibTeX
@misc{pavesi2026model,
title = {{Model Counting as a Sum of Products: Verified Translation and Variable Elimination in Lean 4}},
author = {Luca Eliseo Pavesi},
howpublished = {Zenodo},
year = {2026},
month = oct,
doi = {10.5281/zenodo.23539427},
url = {https://zenodo.org/records/23539427},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Model Counting as a Sum of Products: Verified Translation and Variable Elimination in Lean 4
AU - Luca Eliseo Pavesi
PY - 2026
DA - 2026/10/21
PB - Zenodo
DO - 10.5281/zenodo.23539427
UR - https://zenodo.org/records/23539427
AB - Weighted model counting is the sum, over all assignments of the variables, of a product of clause indicators and literal weights, that is, an einsum over Boolean indices. Tensor-network and project-join model counters build on this view, but the translation from a formula to a sum of products, and the elimination of variables that makes it efficient, are normally trusted. We formalize both in Lean 4, using only its core library, and prove three results. First, the plan of a weighted CNF evaluates to its weighted model count, which is defined independently by enumerating all 2^n assignments. Second, bucket elimination along any order of the variables computes the same count. Third, an eliminated (nested) plan can be flattened to a sum of monomials by a verified compiler that draws bound names from a counter, so that no variable is captured, also when names are reused; composed, these give an end-to-end theorem. The development is executable; on small instances the choice of order changes the number of table entries by up to a factor of six. We make no performance claim against solvers. The record contains the manuscript (LaTeX sources in the format of the Journal on Satisfiability, Boolean Modeling and Computation, and PDF) and the Lean 4 artifact (tic_sat_lean.zip), which builds with "bash build.sh" using Lean 4.35.0.
ER -