OptUx optimal MUS enumerator (pysat.examples.optux
)#
List of classes#
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 isg3
, which stands for Glucose 3 6 (seeSolverNames
). Boolean parametersadapt
,exhaust
, andminz
control whether or not the underlyingRC2
oracles should apply detection and adaptation of intrinsic AtMost1 constraints, core exhaustion, and core reduction. Also, unsatisfiable cores can be trimmed if thetrim
parameter is set to a non-zero integer. Finally, verbosity level can be set using theverbose
parameter.Two additional optional parameters
unsorted
anddcalls
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 usesLBX
directly). Parameterdcalls
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 ofpuresat
can be eitherFalse
, 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 offormula
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 formulasolver (str) – SAT oracle name
adapt (bool) – detect and adapt intrinsic AtMost1 constraints
cover (
CNFPlus
) – CNFPlus formula to cover when doing MUS enumerationdcalls (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
, andtrim
- represent the input and the options for the RC2 solver.- Parameters
formula (
WCNF
) – input formulasolver (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