OptUx optimal MUS enumerator (`pysat.examples.optux`)#

List of classes#

OptUx

A simple Python version of the implicit hitting set based optimal MUS extractor and enumerator.

Module description#

An implementation of an extractor of a smallest size minimal unsatisfiable subset (smallest MUS, or SMUS) [1] [2] [3] [4] and enumerator of SMUSes based on implicit hitting set enumeration [1]. This implementation tries to replicate the well-known SMUS extractor Forqes [1]. In contrast to Forqes, this implementation supports not only plain DIMACS CNF formulas but also weighted WCNF formulas. As a result, the tool is able to compute and enumerate optimal MUSes in case of weighted formulas. On the other hand, this prototype lacks a number of command-line options used in Forqes and so it may be less efficient compared to Forqes but the performance difference should not be significant.

The file provides a class OptUx, which is the basic implementation of the algorithm. It can be applied to any formula in the CNF or WCNF format.

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

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

$ optux.py -vvv formula.wcnf.xz
c mcs: 1 2 0
c mcses: 0 unit, 1 disj
c mus: 1 2 0
c cost: 2
c oracle time: 0.0001

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

>>> from pysat.examples.optux import OptUx
>>> from pysat.formula import WCNF
>>>
>>> wcnf = WCNF(from_file='formula.wcnf.xz')
>>>
>>> with OptUx(wcnf) as optux:
...     for mus in optux.enumerate():
...         print('mus {0} has cost {1}'.format(mus, optux.cost))
mus [1, 2] has cost 2
mus [1, 3] has cost 2
mus [2, 3] has cost 2

As can be seen in the example above, the solver can be instructed either to compute one optimal MUS of an input formula, or to enumerate a given number (or all) of its top optimal MUSes.

Module details#

class examples.optux.OptUx(formula, solver='g3', adapt=False, cover=None, dcalls=False, exhaust=False, minz=False, puresat=False, unsorted=False, trim=False, verbose=0)#

A simple Python version of the implicit hitting set based optimal MUS extractor and enumerator. Given a (weighted) (partial) CNF formula, i.e. formula in the WCNF format, this class can be used to compute a given number of optimal MUS (starting from the best one) of the input formula. OptUx roughly follows the implementation of Forqes [1] but lacks a few additional heuristics, which however aren’t applied in Forqes by default.

As a result, OptUx applies exhaustive disjoint minimal correction subset (MCS) enumeration [1], [2], [3], [4] with the incremental use of RC2 [5] as an underlying MaxSAT solver. Once disjoint MCSes are enumerated, they are used to bootstrap a hitting set solver. This implementation uses Hitman as a hitting set solver, which is again based on RC2.

Note that in the main implicit hitting enumeration loop of the algorithm, OptUx follows Forqes in that it does not reduce correction subsets detected to minimal correction subsets. As a result, correction subsets computed in the main loop are added to Hitman unreduced.

OptUx can use any SAT solver available in PySAT. The default SAT solver to use is g3, which stands for Glucose 3 [6] (see SolverNames). Boolean parameters adapt, exhaust, and minz control whether or not the underlying RC2 oracles should apply detection and adaptation of intrinsic AtMost1 constraints, core exhaustion, and core reduction. Also, unsatisfiable cores can be trimmed if the trim parameter is set to a non-zero integer. Finally, verbosity level can be set using the verbose parameter.

Two additional optional parameters unsorted and dcalls can be used to instruct the tool to enumerate MUSes in the unsorted fashion, i.e. optimal MUSes are not guaranteed to go first. For this, OptUx applies LBX-like MCS enumeration (it uses LBX directly). Parameter dcalls can be applied to instruct the underlying MCS enumerator to apply clause D oracle calls.

Another optional paramater puresat can be used to instruct OptUx to run a purely SAT-based minimal hitting set enumerator, following the ideas of [7]. The value of puresat can be either False, meaning that no pure SAT enumeration is to be done or be equal to 'mgh', 'cd15', or 'lgl' - these are the solvers that support hard phase setting, i.e. user preferences will not be overwritten by the phase saving heuristic [8].

Finally, one more optional input parameter cover is to be used when exhaustive enumeration of MUSes is not necessary and the tool can stop as soon as a given formula is covered by the set of currently computed MUSes. This can be made to work if the soft clauses of formula are of size 1.

Parameters:

formula (WCNFPlus) – (weighted) (partial) CNFPlus formula
solver (str) – SAT oracle name
adapt (bool) – detect and adapt intrinsic AtMost1 constraints
cover (CNFPlus) – CNFPlus formula to cover when doing MUS enumeration
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
unsorted (bool) – apply unsorted MUS enumeration
trim (int) – do core trimming at most this number of times
verbose (int) – verbosity level

_disjoint(formula, solver, adapt, exhaust, minz, trim)#

This method constitutes the preliminary step of the implicit hitting set paradigm of Forqes. Namely, it enumerates all the disjoint minimal correction subsets (MCSes) of the formula, which will be later used to bootstrap the hitting set solver.

Note that the MaxSAT solver in use is RC2. As a result, all the input parameters of the method, namely, formula, solver, adapt, exhaust`, minz, and trim - represent the input and the options for the RC2 solver.

Parameters:

formula (WCNF) – input formula
solver (str) – SAT solver name
adapt (bool) – detect and adapt AtMost1 constraints
exhaust (bool) – exhaust unsatisfiable cores
minz (bool) – apply heuristic core minimization
trim (int) – trim unsatisfiable cores at most this number of times

_process_soft(formula)#

The method is for processing the soft clauses of the input formula. Concretely, it checks which soft clauses must be relaxed by a unique selector literal and applies the relaxation.

Parameters:: formula (WCNF) – input formula

compute()#

This method implements the main look of the implicit hitting set paradigm of Forqes to compute a best-cost MUS. The result MUS is returned as a list of integers, each representing a soft clause index.

Return type:: list(int)

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

enumerate()#

This is generator method iterating through MUSes and enumerating them until the formula has no more MUSes, or a user decides to stop the process.

Return type:: list(int)

oracle_time()#

This method computes and returns the total SAT solving time involved.

Return type:: float

A deletion-based MUS extractor (pysat.examples.musx)

RC2 MaxSAT solver (pysat.examples.rc2)