ApproxMC model counter (pysat.allies.approxmc
)#
List of classes#
A wrapper for ApproxMC, a state-of-the-art approximate model counter. |
Module description#
This module provides interface to ApproxMCv4, a state-of-the-art approximate model counter utilising an improved version of CryptoMiniSat to give approximate model counts to problems of size and complexity that are out of reach for earlier approximate model counters. The original work on ApproxMCv4 has been published in 1 and 2.
- 1
Mate Soos, Kuldeep S. Meel. BIRD: Engineering an Efficient CNF-XOR SAT Solver and Its Applications to Approximate Model Counting. AAAI 2019. pp. 1592-1599
- 2
Mate Soos, Stephan Gocht, Kuldeep S. Meel. Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling. CAV 2020. pp. 463-484
Note that to be functional, the module requires package pyapproxmc
to
be installed:
$ pip install pyapproxmc
The interface gives access to Counter
, which expects a formula in
CNF
as input. Given a few additional (optional) arguments,
including a random seed, tolerance factor \(\varepsilon\), and
confidence \(\delta\), the class can be used to get an approximate
number of models of the formula, subject to the given tolerance factor and
confidence parameter.
Namely, given a CNF formula \(\mathcal{F}\) with \(\#\mathcal{F}\) as the exact number of models, and parameters \(\varepsilon\in(0,1]\) and \(\delta\in[0,1)\), the counter computes and reports a value \(C\), which is an approximate number of models of \(\mathcal{F}\), such that \(\textrm{Pr}\left[\frac{1}{1+\varepsilon}\#\mathcal{F}\leq C\leq (1+\varepsilon)\#\mathcal{F}\right]\geq 1-\delta\).
The implementation can be used as an executable (the list of available
command-line options can be shown using approxmc.py -h
) in the
following way:
$ xzcat formula.cnf.xz
p cnf 20 2
1 2 3 0
3 20 0
$ approxmc.py -p 1,2,3-9 formula.cnf.xz
s mc 448
Alternatively, the algorithm can be accessed and invoked through the
standard import
interface of Python, e.g.
>>> from pysat.allies.approxmc import Counter
>>> from pysat.formula import CNF
>>>
>>> cnf = CNF(from_file='formula.cnf.xz')
>>>
>>> with Counter(cnf) as counter:
... print(counter.counter(projection=range(1, 10))
448
As can be seen in the above example, besides model counting across all the variables in a given input formula, the counter supports projected model counting, i.e. when one needs to approximate the number of models with respect to a given list of variables rather than with respect to all variables appearing in the formula. This feature comes in handy when the formula is obtained, for example, through Tseitin transformation 3 with a number of auxiliary variables introduced.
- 3
G. S. Tseitin. On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic, Part II. pp. 115–125, 1968
Module details#
- class allies.approxmc.Counter(formula=None, seed=1, epsilon=0.8, delta=0.2, verbose=0)#
A wrapper for ApproxMC, a state-of-the-art approximate model counter. Given a formula in
CNF
, this class can be used to get an approximate number of models of the formula, subject to tolerance factorepsilon
and confidence parameterdelta
.Namely, given a CNF formula \(\mathcal{F}\) and parameters \(\varepsilon\in(0,1]\) and \(\delta\in[0,1)\), the counter computes and reports a value \(C\) such that \(\textrm{Pr}\left[\frac{1}{1+\varepsilon}\#\mathcal{F}\leq C\leq (1+\varepsilon)\#\mathcal{F}\right]\geq 1-\delta\). Here, \(\#\mathcal{F}\) denotes the exact model count for formula \(\mathcal{F}\).
The
formula
argument can be left unspecified at this stage. In this case, a user is expected to add all the relevant clauses usingadd_clause()
.An additional parameter a user may want to specify is integer
seed
used by ApproxMC. The value ofseed
is set to1
by default.- Parameters
formula (
CNF
) – CNF formulaseed (int) – integer seed value
epsilon (float) – tolerance factor
delta (float) – confidence parameter
verbose (int) – verbosity level
>>> from pysat.allies.approxmc import Counter >>> from pysat.formula import CNF >>> >>> cnf = CNF(from_file='some-formula.cnf') >>> with Counter(formula=cnf, epsilon=0.1, delta=0.9) as counter: ... num = counter.count() # an approximate number of models
- add_clause(clause)#
The method for adding a clause to the problem formula. Although the input formula can be specified as an argument of the constructor of
Counter
, adding clauses may also be helpful afterwards, on the fly.The clause to add can be any iterable over integer literals.
- Parameters
clause (iterable(int)) – a clause to add
>>> from pysat.allies.approxmc import Counter >>> >>> with Counter() as counter: ... counter.add_clause(range(1, 4)) ... counter.add_clause([3, 20]) ... ... print(counter.count()) 720896
- count(projection=None)#
Given the formula provided by the user either in the constructor of
Counter
or through a series of calls toadd_clause()
, this method runs the ApproxMC counter with the specified values of tolerance \(\varepsilon\) and confidence \(\delta\) parameters, as well as the randomseed
value, and returns the number of models estimated.A user may specify an argument
projection
, which is a list of integers specifying the variables with respect to which projected model counting should be performed. Ifprojection
is left asNone
, approximate model counting is performed wrt. all the variables of the input formula.- Parameters
projection (list(int)) – variables to project on
>>> from pysat.allies.approxmc import Counter >>> from pysat.card import CardEnc, EncType >>> >>> # cardinality constraint with auxiliary variables >>> # there are exactly 70 models for the constraint >>> # over the 8 original variables >>> cnf = CardEnc.equals(lits=range(1, 9), bound=4, encoding=EncType.cardnetwrk) >>> >>> with Counter(formula=cnf, epsilon=0.05, delta=0.95) as counter: ... print(counter.count()) 123840 >>> >>> with Counter(formula=cnf, epsilon=0.05, delta=0.95) as counter: ... print(counter.count(projection=range(1, 8))) 70
- delete()#
Explicit destructor of the internal Counter oracle. Delete the actual counter object and sets it to
None
.