124
W. Wang et al.
initiated complexity theoretic studies of model counting and showed that model
counting is #P-hard [63]. The earliest practical approaches to model counting
such as Relsat [12], were based on extending DPLL approaches. The advent of
CDCL solvers led to the paradigm of combining conflict driven search with component caching leading to the development of solvers such as Cachet [49] and
sharpSAT [56]. Furthermore, Darwiche and Marquis [22] pioneered a knowledgecompilation-based approach, relying on the static partitioning of the solution
space, which led to development of c2d. The recent years have witnessed combination of CDCL and static approaches with solvers such as D4 and DSharp. Recently, Lagniez and Marquis proposed a recursive algorithm, called ProjMC [40],
that exploits the disjunctive decomposition technique pioneered in earlier works
to perform projected model counting. Concurrently, another approach, called
Ganak [50], for projected model counting has been developed that provides
probabilistic exact bounds via usage of universal hash functions. In this work,
we focus on ProjMC due to its ability to provide exact counts and demonstrated
scalability in comparison to other approaches.
The theoretical studies of approximation led to the introduction of PAC style,
also referred to as (ε, δ), guarantees wherein the underlying algorithm returns
an estimate within (1 + ε) factor of the exact count with confidence at least
1 − δ. Stockmeyer [54] demonstrated that PAC guarantees can be achieved by a
probabilistic polynomial Turing machine with access to NP oracle. The practical
exploration of Stockmeyer’s approach was pursued with Gomes et al with the
development of MBound [31] and SampleCount [30]. Chakraborty, Meel, and
Vardi proposed a scalable approximate counter, called ApproxMC, with formal
(ε, δ) guarantees which seeks to combine the advances in SAT solving with design
of efficient universal hash functions.
ApproxMC is now in its third generation, called ApproxMC3. The central
idea behind ApproxMC is to employ universal hash functions, represented by
randomly chosen XOR constraints, to partition the solution space into roughly
equal small cells where every cell can be defined by the original constraints
augmented with randomly chosen XOR constraints. ApproxMC invokes CryptoMinisat [53], a solver designed specifically for combination of CNF and XOR
constraints, to enumerate solutions in a randomly chosen small cell. ApproxMC2
achieves a significant reduction in the number of SAT calls from linear in |S| to
log(|S|) by exploiting dependence among different SAT calls. Soos and Meel
proposed ApproxMC3 by augmenting ApproxMC2 with a new architecture to
handle CNF+XOR formulas [52].
4 Study methodology
This section describes the overall design of our study, including the model counting tools, the generation of constraint solving problems, and the measurements
for evaluation.
4.1 Tools
For approximate model counting, we use ApproxMCv3 (https://github.com/
meelgroup/ApproxMC), which is the latest public release of ApproxMC [52]. For
W. Wang et al.
initiated complexity theoretic studies of model counting and showed that model
counting is #P-hard [63]. The earliest practical approaches to model counting
such as Relsat [12], were based on extending DPLL approaches. The advent of
CDCL solvers led to the paradigm of combining conflict driven search with component caching leading to the development of solvers such as Cachet [49] and
sharpSAT [56]. Furthermore, Darwiche and Marquis [22] pioneered a knowledgecompilation-based approach, relying on the static partitioning of the solution
space, which led to development of c2d. The recent years have witnessed combination of CDCL and static approaches with solvers such as D4 and DSharp. Recently, Lagniez and Marquis proposed a recursive algorithm, called ProjMC [40],
that exploits the disjunctive decomposition technique pioneered in earlier works
to perform projected model counting. Concurrently, another approach, called
Ganak [50], for projected model counting has been developed that provides
probabilistic exact bounds via usage of universal hash functions. In this work,
we focus on ProjMC due to its ability to provide exact counts and demonstrated
scalability in comparison to other approaches.
The theoretical studies of approximation led to the introduction of PAC style,
also referred to as (ε, δ), guarantees wherein the underlying algorithm returns
an estimate within (1 + ε) factor of the exact count with confidence at least
1 − δ. Stockmeyer [54] demonstrated that PAC guarantees can be achieved by a
probabilistic polynomial Turing machine with access to NP oracle. The practical
exploration of Stockmeyer’s approach was pursued with Gomes et al with the
development of MBound [31] and SampleCount [30]. Chakraborty, Meel, and
Vardi proposed a scalable approximate counter, called ApproxMC, with formal
(ε, δ) guarantees which seeks to combine the advances in SAT solving with design
of efficient universal hash functions.
ApproxMC is now in its third generation, called ApproxMC3. The central
idea behind ApproxMC is to employ universal hash functions, represented by
randomly chosen XOR constraints, to partition the solution space into roughly
equal small cells where every cell can be defined by the original constraints
augmented with randomly chosen XOR constraints. ApproxMC invokes CryptoMinisat [53], a solver designed specifically for combination of CNF and XOR
constraints, to enumerate solutions in a randomly chosen small cell. ApproxMC2
achieves a significant reduction in the number of SAT calls from linear in |S| to
log(|S|) by exploiting dependence among different SAT calls. Soos and Meel
proposed ApproxMC3 by augmenting ApproxMC2 with a new architecture to
handle CNF+XOR formulas [52].
4 Study methodology
This section describes the overall design of our study, including the model counting tools, the generation of constraint solving problems, and the measurements
for evaluation.
4.1 Tools
For approximate model counting, we use ApproxMCv3 (https://github.com/
meelgroup/ApproxMC), which is the latest public release of ApproxMC [52]. For