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

List of classes#

MUSX

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.

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 MUSX objects receives a target CNF or .WCNF formula, a SAT solver name, and a verbosity level. Note that the default SAT solver is MiniSat22 (referred to as 'm22', see SolverNames for details). The default verbosity level is 1.

Parameters:

formula (WCNF) – input WCNF formula
solver (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.

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 MUSX class. 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.

An iterative model enumerator (pysat.examples.models)

OptUx optimal MUS enumerator (pysat.examples.optux)

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

List of classes#

Module description#

Module details#

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