ApproxMCCert: Formally Certified Approximate Model Counter

ApproxMCCert is a formally certified approximate model counter utilizing formal proof and a certification pipeline to give certified approximate model counts.

This work is by Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel, to appear in CAV24.

This repository includes the source code of ApproxMCCert, an approximate model counter with certificate generation, and CertCheck, the corresponding certificate checker. The formal proof of the ApproxMC algorithm in Isabelle is available on Archive of Formal Proofs. CertCheck needs access to an external CNF-XOR UNSAT checker, where a CNF-XOR solver CryptoMiniSat outputs the UNSAT proof that is translated and verified by FRAT-xor and cake_xlrup.

If you are only interested in scalable approximate model counting, visit our state-of-the-art counter ApproxMC.

Build

Run the following script to install all dependencies.

./install.sh

Usage

The following script runs ApproxMCCert and outputs a certified approximate count or raises an error.

./run.sh cnf_file

You can find an example below.

./run.sh ./example.cnf