A deletion-based MUS extractor (pysat.examples.musx)#
List of classes#
MUS eXtractor using the deletion-based algorithm. |
Module description#
This module implements a deletion-based algorithm 1 for extracting a minimal unsatisfiable subset (MUS) of a given (unsafistiable) CNF formula. This simplistic implementation can deal with plain and partial CNF formulas, e.g. formulas in the DIMACS CNF and WCNF formats.
- 1(1,2)
Joao Marques-Silva. Minimal Unsatisfiability: Models, Algorithms and Applications. ISMVL 2010. pp. 9-14
The following extraction procedure is implemented:
# oracle: SAT solver (initialized)
# assump: full set of assumptions
i = 0
while i < len(assump):
to_test = assump[:i] + assump[(i + 1):]
if oracle.solve(assumptions=to_test):
i += 1
else:
assump = to_test
return assump
The implementation can be used as an executable (the list of available
command-line options can be shown using musx.py -h) in the following
way:
$ cat formula.wcnf
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
$ musx.py -s glucose3 -vv formula.wcnf
c MUS approx: 1 2 0
c testing clid: 0 -> sat (keeping 0)
c testing clid: 1 -> sat (keeping 1)
c nof soft: 3
c MUS size: 2
v 1 2 0
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.musx import MUSX
>>> from pysat.formula import WCNF
>>>
>>> wcnf = WCNF(from_file='formula.wcnf')
>>>
>>> musx = MUSX(wcnf, verbosity=0)
>>> musx.compute() # compute a minimally unsatisfiable set of clauses
[1, 2]
Note that the implementation is able to compute only one MUS (MUS enumeration is not supported).
Module details#
- class examples.musx.MUSX(formula, solver='m22', verbosity=1)#
MUS eXtractor using the deletion-based algorithm. The algorithm is described in 1 (also see the module description above). Essentially, the algorithm can be seen as an iterative process, which tries to remove one soft clause at a time and check whether the remaining set of soft clauses is still unsatisfiable together with the hard clauses.
The constructor of
MUSXobjects receives a targetWCNFformula, a SAT solver name, and a verbosity level. Note that the default SAT solver is MiniSat22 (referred to as'm22', seeSolverNamesfor details). The default verbosity level is1.- Parameters
formula (
WCNF) – input WCNF formulasolver (str) – name of SAT solver
verbosity (int) – verbosity level
- _compute(approx)#
Deletion-based MUS extraction. Given an over-approximation of an MUS, i.e. an unsatisfiable core previously returned by a SAT oracle, the method represents a loop, which at each iteration removes a clause from the core and checks whether the remaining clauses of the approximation are unsatisfiable together with the hard clauses.
Soft clauses are (de)activated using the standard MiniSat-like assumptions interface 2. Each soft clause \(c\) is augmented with a selector literal \(s\), e.g. \((c) \gets (c \vee \neg{s})\). As a result, clause \(c\) can be activated by assuming literal \(s\). The over-approximation provided as an input is specified as a list of selector literals for clauses in the unsatisfiable core.
- 2
Niklas Eén, Niklas Sörensson. Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4). 2003. pp. 543-560
- Parameters
approx (list(int)) – an over-approximation of an MUS
Note that the method does not return. Instead, after its execution, the input over-approximation is refined and contains an MUS.
- compute()#
This is the main method of the
MUSXclass. It computes a set of soft clauses belonging to an MUS of the input formula. First, the method checks whether the formula is satisfiable. If it is, nothing else is done. Otherwise, an unsatisfiable core of the formula is extracted, which is later used as an over-approximation of an MUS refined in_compute().
- delete()#
Explicit destructor of the internal SAT oracle.
- oracle_time()#
Method for calculating and reporting the total SAT solving time.