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.

1(1,2,3,4,5)

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

2(1,2)

Mark H. Liffiton, Maher N. Mneimneh, Ines Lynce, Zaher S. Andraus, Joao Marques-Silva, Karem A. Sakallah. A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints An Int. J. 14(4). 2009. pp. 415-442

3(1,2)

Alexey Ignatiev, Mikolas Janota, Joao Marques-Silva. Quantified Maximum Satisfiability: A Core-Guided Approach. SAT 2013. pp. 250-266

4(1,2)

Alexey Ignatiev, Mikolas Janota, Joao Marques-Silva. Quantified maximum satisfiability. Constraints An Int. J. 21(2). 2016. pp. 277-302

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.

5

Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva. RC2: an Efficient MaxSAT Solver. J. Satisf. Boolean Model. Comput. 11(1). 2019. pp. 53-64

6

Gilles Audemard, Jean-Marie Lagniez, Laurent Simon. Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction. SAT 2013. pp. 309-317

7

Enrico Giunchiglia, Marco Maratea. Solving Optimization Problems with DLL. ECAI 2006. pp. 377-381

8

Knot Pipatsrisawat, Adnan Darwiche. A Lightweight Component Caching Scheme for Satisfiability Solvers. SAT 2007. pp. 294-299

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

previous

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

next

RC2 MaxSAT solver (pysat.examples.rc2)