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

List of classes

Sampler

A wrapper for UniGen3, a state-of-the-art almost-uniform sampler.

Module description

This module provides interface to UniGen3, a state-of-the-art almost-uniform sampler utilising an improved version of CryptoMiniSat to handle problems of size and complexity that were not possible before. . The original work on UniGen3 has been published in [1], [2], and [3].

[1]

Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi. Balancing Scalability and Uniformity in SAT Witness Generator. DAC 2014. pp. 60:1-60:6

[2] (1,2)

Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi. On Parallel Scalable Uniform SAT Witness Generation. TACAS 2015. pp. 304-319

[3]

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 pyunigen to be installed:

$ pip install pyunigen

The interface gives access to Sampler, which expects a formula in CNF as input. Given a few additional (optional) arguments, including a random seed, tolerance factor \(\varepsilon\), confidence \(\delta\) (to be used by ApproxMC), and uniformity parameter \(\kappa\), the class can be used to get apply almost-uniform sampling and to obtain a requested number of samples as a result, subject to the given tolerance factor and confidence parameter.

Namely, given a CNF formula \(\mathcal{F}\) with the set of satisfying assignments (or models) denoted by \(sol(\mathcal{F})\) and parameter \(\varepsilon\in(0,1]\), a uniform sampler outputs a model \(y\in sol(\mathcal{F})\) such that \(\textrm{Pr}\left[y \textrm{ is output}\right]=\frac{1}{|sol(\mathcal{F})|}\). Almost-uniform sampling relaxes the uniformity guarantee and ensures that \(\frac{1}{(1+\varepsilon)|sol(\mathcal{F})|} \leq \textrm{Pr}\left[y \textrm{ is output}\right] \leq \frac{1+\varepsilon}{|sol(\mathcal{F})|}\).

The implementation can be used as an executable (the list of available command-line options can be shown using unigen.py -h) in the following way:

$ xzcat formula.cnf.xz
p cnf 6 2
1 5 0
1 6 0

$ unigen.py -n 4 formula.cnf.xz
v +1 -2 +3 -4 -5 -6 0
v +1 +2 +3 -4 +5 +6 0
v +1 -2 -3 -4 +5 -6 0
v -1 -2 -3 -4 +5 +6 0

Alternatively, the algorithm can be accessed and invoked through the standard import interface of Python, e.g.

>>> from pysat.allies.unigen import Sampler
>>> from pysat.formula import CNF
>>>
>>> cnf = CNF(from_file='formula.cnf.xz')
>>>
>>> with Sampler(cnf) as sampler:
...     print(sampler.sample(nof_samples=4, sample_over=[1, 2, 3])
[[1, 2, 3, 4, 5], [1, -2, -3, -4, -5], [1, -2, -3, -4, 5], [1, 2, -3, 4, 5]]

As can be seen in the above example, sampling can be done over a user-defined set of variables (rather than the complete set of variables).

Module details

class allies.unigen.Sampler(formula=None, seed=1, epsilon=0.8, delta=0.2, kappa=0.638, verbose=0)

A wrapper for UniGen3, a state-of-the-art almost-uniform sampler. Given a formula in CNF, this class can be used to apply almost-uniform sampling of the formula’s models, subject to a few input parameters.

The class initialiser receives a number of input arguments. 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().

Additional parameters a user may want to specify include integer seed (used by ApproxMC), tolerance factor epsilon (used in the probabilistic guarantees of almost-uniformity), confidence parameter delta (used by ApproxMC), and uniformity parameter kappa (see [2]).

Parameters:

• formula (CNF) – CNF formula

• seed (int) – seed value

• epsilon (float) – tolerance factor

• delta (float) – confidence parameter (used by ApproxMC)

• kappa (float) – uniformity parameter

• verbose (int) – verbosity level

>>> from pysat.allies.unigen import Sampler
>>> from pysat.formula import CNF
>>>
>>> cnf = CNF(from_file='some-formula.cnf')
>>> with Sampler(formula=cnf, epsilon=0.1, delta=0.9) as sampler:
...     for model in sampler.sample(nof_samples=100):
...         print(model)  # printing 100 result samples

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 Sampler, 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.unigen import Sampler
>>>
>>> with Sampler() as sampler:
...     sampler.add_clause(range(1, 4))
...     sampler.add_clause([3, 4])
...
...     print(sampler.sample(nof_samples=4))
[[1, 2, -3, 4], [-1, 2, -3, 4], [1, 2, 3, -4], [-1, 2, 3, 4]]

delete()

Explicit destructor of the internal Sampler oracle. Delete the actual sampler object and sets it to None.

sample(nof_samples, sample_over=None, counts=None)

Given the formula provided by the user either in the constructor of Sampler or through a series of calls to add_clause(), this method runs the UniGen3 sampler with the specified values of tolerance \(\varepsilon\), confidence \(\delta\) parameters, and uniformity parameter \(kappa\) as well as the random seed value, and outputs a requested number of samples.

A user may specify an argument sample_over, which is a list of integers specifying the variables with respect to which sampling should be performed. If sample_over is left as None, almost-uniform sampling is done wrt. all the variables of the input formula.

Finally, argument counts can be specified as a pair of integer values: cell count and hash count (in this order) used during sampling. If left undefined (None), the values are determined by ApproxMC.

Parameters:

• nof_samples (int) – number of samples to output

• sample_over (list(int)) – variables to sample over

• counts ([int, int]) – cell count and hash count values

Returns:

a list of samples

>>> from pysat.allies.unigen import Sampler
>>> from pysat.card import CardEnc, EncType
>>>
>>> # cardinality constraint with auxiliary variables
>>> # there are exactly 6 models for the constraint
>>> # over the 6 original variables
>>> cnf = CardEnc.equals(lits=range(1, 5), bound=2, encoding=EncType.totalizer)
>>>
>>> with Sampler(formula=cnf, epsilon=0.05, delta=0.95) as sampler:
...     for model in sampler.sample(nof_samples=3):
...         print(model)
[1, -2, 3, -4, 5, 6, -7, -8, 9, -10, 11, -12, 13, 14, -15, 16, 17, -18, 19, -20]
[1, -2, -3, 4, 5, 6, -7, -8, 9, -10, 11, -12, 13, 14, -15, 16, 17, -18, 19, -20]
[1, 2, -3, -4, 5, 6, -7, 8, -9, -10, 11, 12, 13, 14, -15, 16, 17, 18, -19, -20]
>>>
>>> # now, sampling over the original variables
>>> with Sampler(formula=cnf, epsilon=0.05, delta=0.95) as sampler:
...     for model in sampler.sample(nof_samples=3, sample_over=range(1, 5)):
...         print(model)
[1, 2, -3, -4]
[1, -2, 3, -4]
[-1, 2, 3, -4]

previous

ApproxMC model counter (pysat.allies.approxmc)