count-catcher: Lean Theorems from Model Counting Certificates

Abstract

We present count-catcher, a tool that turns a CPOG certificate of a count by the exact model counter d4 into a Lean theorem that a CNF formula defined in Lean has exactly N models over V variables. With an encoding lemma, this theorem becomes a theorem about the number of combinatorial objects. A CPOG certificate consists of a Boolean circuit equivalent to the formula and a proof of equivalence. count-catcher checks in Lean that the formula implies the circuit (forward check) and the circuit implies the formula (reverse check). For the forward check, lrat-catcher streams a refutation through the LRAT checker of Lean's standard library. The reverse check and the validity check of the circuit are computations proved correct in Lean. Lean runs all three checks as compiled code, so the theorem depends on Lean's kernel, compiler and runtime, as does CPOG's verified checker. We combine the theorem with results from Mathlib, for instance with Burnside's lemma to count graphs up to isomorphism. We prove the number of Latin squares of order 8 as a weighted sum of hundreds of certified counts from about eight terabytes of certificates. We turn about half of the 2022 Model Counting Competition formulas into theorems, with the three checks taking about a quarter of the time of CPOG's verified checker. We found that CPOG's unverified checker reported wrong counts, and removed its verified checker's dependence on two unproved lemmas. End to end, a theorem costs about the same as a checked count.