BaxMC: a CEGAR approach to Max#SAT (FMCAD22)

The Max#SAT problem is defined as follows: given a propositionnal formula $\phi(X, Y, Z)$, find $x_m$ such that the model counting of $\phi$, projected on $Y$ is maximal.

We propose in this paper a CEGAR-based algorithm to solve this problem, along with proofs of correctness assuming both exact and approximate model counting oracles.

Along with this, we devise an alternate hardness proof of the problem and its generalizations.

Artifacts

We provide some artifacts to reproduce our experiments.

Docker Image

To get the docker image, please follow the instructions here.

After the docker has been downloaded and started, you can run the bencmarks using:

tar -xzvf /benchmarks.tar.gz
baxmc --help
baxmc $BENCHMARK_PATH

The benchmarks can be found in the /benchmarks/ folder.

We also provide a reimplementation of MaxCount in the /maxcount.py file. To use it in the docker image, do:

python3 maxcount.py [epsilon] [delta] [file]

Sources

The source code is accessible here.

This project uses nix to pull the dependencies.

The build process is explicited in the README.md file.

If you have any question, feel free to contact me:

thomas DOT vigouroux AT univ-grenoble-alpes.fr