Primer-B algorithm for prime enumeration (`pysat.examples.primer`)#

List of classes#

Primer

A simple Python-based reimplementation of the Primer-B algorithm.

Module description#

A reimplementation of the prime implicant (and implicate) enumeration algorithm originally called Primer-B [1]. The algorithm exploits the minimal hitting duality between prime implicants and implicates of an input formula and hence makes extensive use of a hitting set enumerator. The input formula can be in a clausal or a non-clausal form, i.e. the input can be given as an object of either CNF or Formula.

The implementation relies on Hitman and supports both sorted and unsorted hitting set enumeration. In the former case, hitting sets are computed from smallest to largest, which is achieved with MaxSAT-based hitting set enumeration, using RC2 [2] [3] [4]. In the latter case, either an LBX-like MCS enumerator LBX [5] is used or pure SAT-based minimal model enumeration [6].

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

$ xzcat formula.cnf.xz
p cnf 4 3
1 2 4 0
1 -2 3 0
-1 2 -4 0

$ primer.py -i -e all formula.cnf.xz
v +1 +2 0
v +2 +3 0
v +1 -4 0
v -1 +3 +4 0
v -1 -2 +4 0
c primes: 5
c oracle time: 0.0001
c oracle calls: 41

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

>>> from pysat.examples.primer import Primer
>>> from pysat.formula import CNF
>>>
>>> cnf = CNF(from_file='test.cnf.xz')
>>>
>>> with Primer(cnf, implicates=False) as primer:
...     for p in primer.enumerate():
...         print(f'prime: {p}')
...
prime: [2, 3]
prime: [1, 2]
prime: [1, -4]
prime: [-1, 3, 4]
prime: [-1, -2, 4]

The tool can be instructed to enumerate either prime implicates or prime implicants (a set of the dual primes covering the formula is computed as a by-product of Primer’s implicit hitting set algorithm). Namely, it targets implicate enumeration by default; setting the Boolean parameter implicates=False will force it to focus on prime implicants instead. (In the command line, the same effect can be achieved if using the option ‘-i’.)

A user may also want to compute \(k\) primes instead of enumerating them exhaustively. This may come in handy, for example, if the input formula has an exponential number of primes. Command-line option -e NUM is responsible for this. In the case of complete prime implicant enumeration the algorithm will essentially end up computing the input formula’s Blake Canonical Form (BCF) [7].

Module details#

class examples.primer.Primer(formula, negated=None, solver='cd19', implicates=True, adapt=False, dcalls=False, exhaust=False, minz=False, puresat=False, search='lin', unsorted=False, trim=False, verbose=0)#

A simple Python-based reimplementation of the Primer-B algorithm. It can be used for computing either \(k\) prime implicates or implicants of an input formula, or enumerating them all exhaustively As the algorithm is based on implicit hitting set enumeration, a set of dual primes (either prime implicants or implicates) covering the input formula is computed as a by-product.

The input formula can be specified either in CNF or be a generic Boolean Formula. In the latter case, the implementation will clausify the formula and, importantly, report all the primes using the integer variable IDs introduced by the clausification process. As a result, a user is assumed responsible for translating these back to the original Atom objects, should the need arise.

Additionally, the user may additionally specify the negation of the formula (if not, Primer will create one in the process) and a few input parameters controlling the run of the algorithm. All of these in fact relate to the parameters of the hitting set enumerator, which is the key component of the tool.

Namely, a user may specify the SAT solver of their choice to be used by Hitman and the two extra SAT oracles as well as set the parameters of MaxSAT/MCS/SAT-based hitting set enumeration. For details on these parameters and what exactly they control, please refer to to the description of Hitman.

Finally, when the algorithm determines a hitting set not to be a target prime, a model is extracted evidencing this fact, which is then reduced into a dual prime. The reduction process is based on MUS extraction and can involve a linear literal traversal or dichotomic similar to the ideas of QuickXPlain [8]. The choice of the type of literal traversal can be made using the search parameter, which can be set either to 'lin' or 'bin'.

The complete list of input parameters is as follows:

Parameters:

formula (Formula or CNF) – input formula whose prime representation is sought
negated (Formula or CNF) – input’s formula negation (if any)
solver (str) – SAT oracle name
implicates (bool) – whether or not prime implicates to target
adapt (bool) – detect and adapt intrinsic AtMost1 constraints
dcalls (bool) – apply clause D oracle calls (for unsorted enumeration only)
exhaust (bool) – do core exhaustion
minz (bool) – do heuristic core reduction
puresat (str) – use pure SAT-based hitting set enumeration
search (str) – dual prime reduction strategy
unsorted (bool) – apply unsorted MUS enumeration
trim (int) – do core trimming at most this number of times
verbose (int) – verbosity level

compute()#

Computes a single prime. Performs as many iterations of the Primer-B algorithm as required to get the next prime. This often involves the computation of the dual cover of the formula.

Returns a list of literals included in the result prime.

Return type:: list(int)

delete()#: Explicit destructor of the internal hitting set enumerator and the SAT oracles.

enumerate()#

This is generator method iterating through primes and enumerating them until the formula has no more primes, or a user decides to stop the process (this is controlled from the outside).

Return type:: list(int)

init_oracles()#

Encodes the formula in dual-rail representation and initialises the hitting set enumerator as well as the two additional SAT oracles.

In particular, this method initialises the hitting set enumerator with the dual-rail clauses \((\neg{p_i} \vee \neg{n_i})\) for each variable \(v_i\) of the formula. Additionally, the two SAT oracles (prime checker and dual reducer) are fed the input formula and its negation, or the other way around (depending on whether the user aims at enumerating implicates of implicants).

Given the above, the method necessarily creates a clausal representation of both the original formula and its negation,

minimise_dual(core)#

Reduces a dual prime from the model of the checker oracle. The procedure is initialised with the over-approximation of a prime and builds on simple MUS extraction. Hence the name of the input parameter to start from: core. The result of this method is a dual prime.

The method traverses the dual to reduce either in the linear fashion or runs dichotomic QuickXPlain-like literal traversal. This is controlled by the input parameter search passed to the constructor of Primer.

Return type:: list(int)

oracle_time()#

This method computes and returns the total SAT solving time involved, including the time spent by the hitting set enumerator and the two SAT oracles.

Return type:: float