Bica algorithm for formula simplification (pysat.examples.bica)

List of classes

Bica	A simple reimplementation of the Bica algorithm.

Module description

A reimplementation of the Bica algorithm for SAT-based minimisation / simplification of Boolean formulas [1]. Given an arbitrary Boolean formula, it computes its smallest size prime cover, i.e. it constructs a smallest CNF (DNF, resp.) representation comprising the formula’s prime implicates (implicants, reps.), which is equivalent to the original formula.

The original Bica algorithm is inspired by the well-known Quine-McCluskey algorithm [2] [3] [4]. It is entirely SAT-based and can deal with arbitrary Boolean formulas. The algorithm involves two steps: first, it enumerates all the prime implicants (or implicates, depending on the user’s choice) of the formula by utilising the Primer algorithm [5]; second, it computes the formula’s smallest prime cover by means of reducing the problem to the computation of a smallest minimal unsatisfiable subformula (SMUS), invoking the OptUx SMUS solver [6].

The word “bica” is Portuguese and means a cup of extremely strong and high-quality coffee (often seen as a synonym of espresso). This way, the Bica algorithm continues the coffee inspiration of the Espresso logic minimizer [7], hence signifying the construction of the formula’s essence or crux. (In fact, this reimplementation was initially planned to have the name Crux, to relate with one of the most prominent constellations of the southern sky, often used in navigation to determine the Southern Celestial Pole.)

[1]

Alexey Ignatiev, Alessandro Previti, Joao Marques-Silva. SAT-Based Formula Simplification. SAT 2015. pp. 287-298

[2]

Willard V. Quine. The Problem of Simplifying Truth Functions. American Mathematical Monthly 59(8). 1952. pp. 521-531

[3]

Willard V. Quine. A Way to Simplify Truth Functions. American Mathematical Monthly 62(9). 1955. pp. 627-631

[4]

Edward J. McCluskey. Minimization of Boolean Functions. Bell System Technical Journal 35(6). 1956. pp 1417-1444

[5]

Alessandro Previti, Alexey Ignatiev, António Morgado, Joao Marques-Silva. Prime Compilation of Non-Clausal Formulae. IJCAI 2015. pp. 1980-1988

[6]

Alexey Ignatiev, Alessandro Previti, Mark H. Liffiton, Joao Marques-Silva. Smallest MUS Extraction with Minimal Hitting Set Dualization. CP 2015. pp. 173-182

[7]

Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli,, Curtis T. McMullen, Gary D. Hachtel. Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic Publishers. 1984

The file provides a class Bica, which contains the above algorithm reimplementation. It can be applied to any formula in the CNF or Formula format.

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

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

$ bica.py -v formula.cnf.xz
c prime -1 +2 0
c prime +1 -2 0
c prime +1 -3 +4 0
c prime +2 -3 +4 0
c prime +1 +3 -4 0
c prime +2 +3 -4 0
c prime +1 +3 -5 +6 0
c prime +1 +3 +5 -6 0
c prime +1 +3 +5 +7 0
c prime +1 +3 +6 +7 0
c prime +1 +4 +5 +7 0
c prime +1 +4 +6 +7 0
c prime +1 +4 +5 -6 0
c prime +1 +4 -5 +6 0
c prime +2 +4 -5 +6 0
c prime +2 +3 -5 +6 0
c prime +2 +3 +5 -6 0
c prime +2 +4 +5 -6 0
c prime +2 +3 +5 +7 0
c prime +2 +4 +5 +7 0
c prime +2 +3 +6 +7 0
c prime +2 +4 +6 +7 0
p cnf 7 7
-1 2 0
1 -2 0
2 -3 4 0
2 3 -4 0
2 3 -5 6 0
2 4 5 -6 0
2 4 6 7 0
o 7
c primer time: 0.0002
c optux  time: 0.0001
c total  time: 0.0004

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

>>> from pysat.examples.bica import Bica
>>> from pysat.formula import Atom, CNF, Formula
>>>
>>> x, y, z = [Atom(v + 1) for v in range(3)]
>>> formula = ~(~x >> y) | (x & z)
>>>
>>> with Bica(formula) as bica:
...     for minf in bica.enumerate():
...         minf = CNF(from_clauses=[bica.primes[i - 1] for i in minf])
...         print(minf)
CNF(from_string='p cnf 3 2\n-1 3 0\n-2 1 0')

As the example above demonstrates, Bica can enumerate all irreducible prime covers of an input formula (or as many as the user wants). In this particular example, the formula \(f\triangleq\neg{(\neg{x} \rightarrow y)} \vee (x \wedge z)\) has the only irreducible prime cover \((\neg{x} \vee z) \vee (\neg{y} \vee x)\).

Module details

class examples.bica.Bica(formula, negated=None, target='cnf', psolver='cd19', padapt=False, pdcalls=False, pexhaust=False, pminz=False, ppuresat=False, psearch='lin', punsorted=False, ptrim=False, osolver='mgh', oadapt=False, odcalls=False, oexhaust=False, ominz=False, onodisj=False, opuresat=False, ounsorted=False, otrim=False, weighted=False, verbose=0)

A simple reimplementation of the Bica algorithm. Although the original implementation of Bica was also written in Python, both phases of the algorithm (prime enumeration and prime cover computation) were written in C++ and interfaced through the file IO. The current implementation relies on pure Python alternatives for both of the phases. Namely, it first calls Primer to enumerate all the primes of a given input formula followed by the computation of a smallest size cover with OptUx.

Importantly, thanks to the capabilities of OptUx, the current implementation allows one to enumerate multiple (or all) smallest size prime covers. Alternatively, one can even opt for computing a minimal prime cover (not a minimum one).

The second phase of the approach also allows a user to compute the target representation either unweighted or weighted. In the former case, the size is measured as the number of primes included in the minimal representation. In the latter case, the lenght of each prime is taken into account such that the overall size is counted as the sum of lengths of the primes included. This is controlled with the use of input parameter weighted.

Additionally, one may additionally want to specify the negation of the input formula, which is required either in first phase of the algorithm or in both phases, depending on whether the user wants to compute a DNF or CNF representation. If no negated formula is provided, Bica will create one internally.

As both phases of the algorithm rely on implicit hitting set enumeration, they share the same input parameters. To allow a user to apply various parameters for the two phases, Hitman’s parameters of the Primer phase are prefixed with a p while the same parameters used by OptUx are prefixed with an o.

The complete list of initialiser’s arguments 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)

• target (str) – either 'cnf' or 'dnf'

• psolver (str) – SAT oracle name

• padapt (bool) – detect and adapt intrinsic AtMost1 constraints

• pdcalls (bool) – apply clause D oracle calls (for unsorted enumeration only)

• pexhaust (bool) – do core exhaustion

• pminz (bool) – do heuristic core reduction

• ppuresat (str) – use pure SAT-based hitting set enumeration

• psearch (str) – dual prime reduction strategy

• punsorted (bool) – apply unsorted MUS enumeration

• ptrim (int) – do core trimming at most this number of times

• osolver (str) – SAT oracle name

• oadapt (bool) – detect and adapt intrinsic AtMost1 constraints

• odcalls (bool) – apply clause D oracle calls (for unsorted enumeration only)

• oexhaust (bool) – do core exhaustion

• ominz (bool) – do heuristic core reduction

• onodisj (bool) – do not enumerate disjoint MCSes with OptUx

• opuresat (str) – use pure SAT-based hitting set enumeration

• ounsorted (bool) – apply unsorted MUS enumeration

• otrim (int) – do core trimming at most this number of times

• weighted (bool) – get a minimal cover wrt. the total number of literals

• verbose (int) – verbosity level

compute()

Computes a single minimum representation of the input formula as a list of indices of prime implicants (or implicates) determined to comprise the representation.

Note that the indices in the returned list start from 1, i.e. the user is supposed to subtract 1 for each of them to get the correct list of primes. Consider the following example:

>>> from pysat.examples.bica import Bica
>>> from pysat.formula import CNF
>>>
>>> cnf = CNF(from_clauses=[[-1, 2], [-2, 3], [-3, 4], [4, 5]])
>>>
>>> with Bica(formula) as bica:
...     for minf in bica.enumerate():
...         minf = CNF(from_clauses=[bica.primes[i - 1] for i in minf])
...         print(minf)
...     print(f'all primes implicates: {bica.primes}')
CNF(from_string='p cnf 4 3\n4 0\n-2 3 0\n-1 2 0')
all prime implicates: [[4], [-2, 3], [-1, 3], [-1, 2]]

Return type:

list(int)

delete()

Explicit destructor of both primer and optux. Also, clears the list of primes computed.

(The former is constructed in Bica’s initialiser while the latter is created on demand, once the first phase of the algorithm has been finished, i.e. when all the primes have been enumerated.)

enumerate()

This is generator method iterating through minimum representations and enumerating them until no more of them exists, or a user decides to stop the process.

>>> from pysat.examples.bica import Bica
>>> from pysat.formula import *
>>>
>>> cnf = CNF(from_file='test.cnf')
>>> print(cnf)
CNF(from_string='c n orig vars 5\np cnf 11 5\n-1 2 0\n1 -2 0\n1 2 -3 4 0\n1 2 3 -4 0\n1 2 3 4 5 0')
>>>
>>> with Bica(cnf) as bica:
...     for minf in bica.enumerate():
...         print(minf)  # prime indices start from 1!
[1, 2, 8, 9, 10]
[1, 2, 3, 8, 10]
[1, 2, 3, 6, 10]
[1, 2, 3, 4, 8]
[1, 2, 3, 4, 6]
[1, 2, 4, 7, 8]
[1, 2, 4, 8, 9]
[1, 2, 4, 5, 8]
[1, 2, 4, 6, 7]
[1, 2, 4, 5, 6]
[1, 2, 4, 6, 9]
[1, 2, 6, 7, 10]
[1, 2, 7, 8, 10]
[1, 2, 5, 8, 10]
[1, 2, 5, 6, 10]
[1, 2, 6, 9, 10]

Return type:

list(int)

oracle_time()

This method computes and returns the total SAT solving time involved, including the time spent by Primer and OptUx, which implement the first and second phases of the algorithm, respectively.

Return type:

float