# Approximate Model Counting, Sparse XOR Constraints and Minimum Distance

## TL;DR

This paper investigates the use of sparse XOR constraints in approximate model counting, linking the effectiveness of these constraints to the geometric structure of model sets, especially minimum Hamming distance.

## Contribution

It introduces a theoretical analysis connecting sparse XOR constraints to model set geometry, providing insights for improving approximate counting methods.

## Key findings

- Sparse XOR constraints can be effectively used with guarantees of correctness.
- The bounds depend on the minimum Hamming distance between models.
- Theoretical results are validated on specific Boolean formulas.

## Abstract

The problem of counting the number of models of a given Boolean formula has numerous applications, including computing the leakage of deterministic programs in Quantitative Information Flow. Model counting is a hard, #P-complete problem. For this reason, many approximate counters have been developed in the last decade, offering formal guarantees of confidence and accuracy. A popular approach is based on the idea of using random XOR constraints to, roughly, successively halving the solution set until no model is left: this is checked by invocations to a SAT solver. The effectiveness of this procedure hinges on the ability of the SAT solver to deal with XOR constraints, which in turn crucially depends on the length of such constraints. We study to what extent one can employ sparse, hence short, constraints, keeping guarantees of correctness. We show that the resulting bounds are closely related to the geometry of the set of models, in particular to the minimum Hamming distance between models. We evaluate our theoretical results on a few concrete formulae. Based on our findings, we finally discuss possible directions for improvements of the current state of the art in approximate model counting.