ApproxMC model counter (pysat.allies.approxmc)#

List of classes#

Counter

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].

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.

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 factor epsilon and confidence parameter delta.

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 using add_clause().

An additional parameter a user may want to specify is integer seed used by ApproxMC. The value of seed is set to 1 by default.

Parameters:

  • formula (CNF) – CNF formula

  • seed (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 to add_clause(), this method runs the ApproxMC counter with the specified values of tolerance \(\varepsilon\) and confidence \(\delta\) parameters, as well as the random seed 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. If projection is left as None, 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.

previous

RC2 MaxSAT solver (pysat.examples.rc2)

next

UniGen almost-uniform sampler (pysat.allies.unigen)