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 assumptionsi=0whilei<len(assump):to_test=assump[:i]+assump[(i+1):]iforacle.solve(assumptions=to_test):i+=1else:assump=to_testreturnassump
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.
>>> frompysat.examples.musximportMUSX>>> frompysat.formulaimportWCNF>>>>>> 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).
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.
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.
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().