This module implements a prototype of the LBX algorithm for the computation
of a minimal correction subset (MCS) and/or MCS enumeration. The LBX
abbreviation stands for literal-based MCS extraction algorithm, which was
proposed in [1]. Note that this prototype does not follow the original
low-level implementation of the corresponding MCS extractor available
online (compared to
our prototype, the low-level implementation has a number of additional
heuristics used). However, it implements the LBX algorithm for partial
MaxSAT formulas, as described in [1].
The implementation can be used as an executable (the list of available
command-line options can be shown using lbx.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
$ lbx.py -d -e all -s glucose3 -vv formula.wcnf.xz
c MCS: 1 3 0
c cost: 2
c MCS: 2 3 0
c cost: 2
c MCS: 1 2 0
c cost: 2
c oracle time: 0.0002
Alternatively, the algorithm can be accessed and invoked through the
standard import interface of Python, e.g.
LBX-like algorithm for computing MCSes. Given an unsatisfiable partial
CNF formula, i.e. formula in the WCNF format, this class can
be used to compute a given number of MCSes of the formula. The
implementation follows the LBX algorithm description in [1]. It can
use any SAT solver available in PySAT. Additionally, the “clause
\(D\)” heuristic can be used when enumerating MCSes.
The default SAT solver to use is m22 (see SolverNames).
The “clause \(D\)” heuristic is disabled by default, i.e.
use_cld is set to False. Internal SAT solver’s timer is also
disabled by default, i.e. use_timer is False.
Parameters:
formula (WCNF) – unsatisfiable partial CNF formula
use_cld (bool) – whether or not to use “clause \(D\)”
solver_name (str) – SAT oracle name
use_timer (bool) – whether or not to use SAT solver’s timer
The main method of the class, which computes an MCS given its
over-approximation. The over-approximation is defined by a model
for the hard part of the formula obtained in compute().
The method is essentially a simple loop going over all literals
unsatisfied by the previous model, i.e. the literals of
self.setd and checking which literals can be satisfied. This
process can be seen a refinement of the over-approximation of the
MCS. The algorithm follows the pseudo-code of the LBX algorithm
presented in [1].
Additionally, if LBX was constructed with the requirement
to make “clause \(D\)” calls, the method calls
do_cld_check() at every iteration of the loop using the
literals of self.setd not yet checked, as the contents of
“clause \(D\)”.
This method extracts a model provided by the previous call to a SAT
oracle and iterates over all soft clauses checking if each of is
satisfied by the model. Satisfied clauses are marked accordingly
while the literals of the unsatisfied clauses are kept in a list
called setd, which is then used to refine the correction set
(see _compute(), and do_cld_check()).
Optional Boolean parameter update_setd enforces the method to
update variable self.setd. If this parameter is set to
False, the method only updates the list of satisfied clauses,
which is an under-approximation of a maximal satisfiable subset
(MSS).
Parameters:
update_setd (bool) – whether or not to update setd
Map an external variable to an internal one if necessary.
This method is used when new clauses are added to the formula
incrementally, which may result in introducing new variables
clashing with the previously used clause selectors. The method
makes sure no clash occurs, i.e. it maps the original variables
used in the new problem clauses to the newly introduced auxiliary
variables (see add_clause()).
Given an integer literal, a fresh literal is returned. The returned
integer has the same sign as the input literal.
Given a clause (as an iterable of integers) and an assignment (as a
list of integers), this method checks whether or not the assignment
satisfies the clause. This is done by a simple clause traversal.
The method is invoked from _filter_satisfied().
The method for adding a new hard of soft clause to the problem
formula. Although the input formula is to be specified as an
argument of the constructor of LBX, adding clauses may be
helpful when enumerating MCSes of the formula. This way, the
clauses are added incrementally, i.e. on the fly.
The clause to add can be any iterable over integer literals. The
additional Boolean parameter soft can be set to True
meaning the the clause being added is soft (note that parameter
soft is set to False by default).
Also note that besides pure clauses, the method can also expect
native cardinality constraints represented as a pair (lits,bound). Only hard cardinality constraints can be added.
Block a (previously computed) MCS. The MCS should be given as an
iterable of integers. Note that this method is not automatically
invoked from enumerate() because a user may want to block
some of the MCSes conditionally depending on the needs. For
example, one may want to compute disjoint MCSes only in which case
this standard blocking is not appropriate.
Compute and return one solution. This method checks whether the
hard part of the formula is satisfiable, i.e. an MCS can be
extracted. If the formula is satisfiable, the model computed by the
SAT call is used as an over-approximation of the MCS in the
method _compute() invoked here, which implements the LBX
algorithm.
An MCS is reported as a list of integers, each representing a soft
clause index (the smallest index is 1).
An optional input parameter is enable, which represents a
sequence (normally a list) of soft clause indices that a user
would prefer to enable/satisfy. Note that this may result in an
unsatisfiable oracle call, in which case None will be reported
as solution. Also, the smallest clause index is assumed to be
1.
Parameters:
enable (iterable(int)) – a sequence of clause ids to enable
Do the “clause \(D\)” check. This method receives a list of
literals, which serves a “clause \(D\)” [2], and checks
whether the formula conjoined with \(D\) is satisfiable.
If clause \(D\) cannot be satisfied together with the formula,
then negations of all of its literals are backbones of the formula
and the LBX algorithm can stop. Otherwise, the literals satisfied
by the new model refine the MCS further.
Every time the method is called, a new fresh selector variable
\(s\) is introduced, which augments the current clause
\(D\). The SAT oracle then checks if clause \((D \vee
\neg{s})\) can be satisfied together with the internal formula.
The \(D\) clause is then disabled by adding a hard clause
\((\neg{s})\).
This method iterates through MCSes enumerating them until the
formula has no more MCSes. The method iteratively invokes
compute(). Note that the method does not block the MCSes
computed - this should be explicitly done by a user.