Collection of backbone computation algorithms (pysat.examples.bbscan)#

List of classes#

BBScan

A solver for computing all backbone literals of a given Boolean formula.

Module description#

A simple implementation of a few backbone extraction algorithms described in [1]. Given a Boolean formula \(\varphi\), a backbone literal is a literal that holds true in every satisfying assignment of \(\varphi\). The backbone of formula \(\varphi\) is the set of all backbone literals. This implementation includes the following algorithms from [1]:

  • implicant enumeration algorithm,

  • iterative algorithm (with one test per variable),

  • complement of backbone estimate algorithm,

  • chunking algorithm,

  • core-based algorithm,

  • core-based algorithm with chunking.

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

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

$ bbscan.py -v formula.cnf.xz
c formula: 3 vars, 4 clauses
c using iterative algorithm
v +1 -3 0
c backbone size: 2 (66.67% of all variables)
c oracle time: 0.0000
c oracle calls: 4

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

>>> from pysat.examples.bbscan import BBScan
>>> from pysat.formula import CNF
>>>
>>> # reading a formula from file
>>> cnf = CNF(from_file='formula.wcnf.xz')
>>>
>>> # creating BBScan and running it
>>> with BBScan(cnf, solver='g3', lift=False, rotate=True) as bbscan:
...     bbone = bbscan.compute(algorithm='core')
...
...     # outputting the results
...     if bbone:
...         print(bbone)
[1, -3]

Each of the available algorithms can be augmented with two simple heuristics aiming at reducing satisfying assignments and, thus, filtering out unnecessary literals: literal lifting and filtering rotatable literals. Both are described in the aforementioned paper.

Note that most of the methods of the class BBScan are made private. Therefore, the tool provides a minimalistic interface via which a user can specify all the necessary parameters.

Module details#

class examples.bbscan.BBScan(formula, solver='g3', lift=False, rotate=False, verbose=0)#

A solver for computing all backbone literals of a given Boolean formula. It implements 6 algorithms for backbone computation described in [1] augmented with two simple heuristics that can be speed up the process.

Note that the input formula can be a CNF object but also any object of class Formula, thus the tool can used for computing backbone literals of non-clausal formulas.

A user can select one of the SAT solvers available at hand ('glucose3' is used by default). The optional two heuristics can be also specified as Boolean input arguments lift, and rotate (turned off by default).

The list of initialiser’s arguments is as follows:

Parameters:

  • formula (Formula or CNF) – input formula whose backbone is sought

  • solver (str) – SAT oracle name

  • lift (bool) – apply literal lifting heuristic

  • rotate (bool) – apply rotatable literal filtering

  • verbose (int) – verbosity level

compute(algorithm='iter', chunk_size=100, focus_on=None)#

Main solving method. A user is supposed to specify which backbone computation algorithm they want to use:

  • 'enum' (implicant enumeration algorithm),

  • 'iter' (iterative algorithm, with one test per variable),

  • 'compl' (complement of backbone estimate algorithm),

  • 'chunk' (chunking algorithm),

  • 'core' (core-based algorithm),

  • 'corechunk' (core-based algorithm with chunking).

By default, BBScan opts for 'iter'.

If the chunking algorithm is selected (either 'chunk' or 'corechunk'), the user may specify the size of the chunk, which is set to 100 by default. Note that the chunk_size can be a floating-point number in the interval (0, 1], which will set the actual chunk_size relative to the total number of literals of interest.

Finally, one may opt for computing backbone literals out of a particular subset of literals, which may run faster than computing the entire formula’s backbone. To focus on a particular set of literals, the user should use the parameter focus_on, which is set to None by default.

Note

The method raises ValueError if the input formula is unsatisfiable.

Parameters:

  • algorithm (str) – backbone computation algorithm

  • chunk_size (int or float) – number of literals in the chunk (for chunking algorithms)

  • focus_on (iterable(int)) – a list of literals to focus on

delete()#

Explicit destructor of the internal SAT oracle.

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