LBX-like MCS enumerator (pysat.examples.lbx
)#
List of classes#
LBX-like algorithm for computing MCSes. |
Module description#
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.
- 1(1,2,3,4)
Carlos Mencia, Alessandro Previti, Joao Marques-Silva. Literal-Based MCS Extraction. IJCAI 2015. pp. 1973-1979
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.
>>> from pysat.examples.lbx import LBX
>>> from pysat.formula import WCNF
>>>
>>> wcnf = WCNF(from_file='formula.wcnf.xz')
>>>
>>> lbx = LBX(wcnf, use_cld=True, solver_name='g3')
>>> for mcs in lbx.enumerate():
... lbx.block(mcs)
... print(mcs)
[1, 3]
[2, 3]
[1, 2]
Module details#
- class examples.lbx.LBX(formula, use_cld=False, solver_name='m22', use_timer=False)#
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
(seeSolverNames
). The “clause \(D\)” heuristic is disabled by default, i.e.use_cld
is set toFalse
. Internal SAT solver’s timer is also disabled by default, i.e.use_timer
isFalse
.- Parameters
formula (
WCNF
) – unsatisfiable partial CNF formulause_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
- _compute()#
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 callsdo_cld_check()
at every iteration of the loop using the literals ofself.setd
not yet checked, as the contents of “clause \(D\)”.
- _filter_satisfied(update_setd=False)#
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()
, anddo_cld_check()
).Optional Boolean parameter
update_setd
enforces the method to update variableself.setd
. If this parameter is set toFalse
, 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_extlit(l)#
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.
- Parameters
l (int) – literal to map
- Return type
int
- _satisfied(cl, model)#
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()
.- Parameters
cl (iterable(int)) – a clause to check
model (list(int)) – an assignment
- Return type
bool
- add_clause(clause, soft=False)#
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 toTrue
meaning the the clause being added is soft (note that parametersoft
is set toFalse
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.- Parameters
clause (iterable(int)) – a clause to add
soft (bool) – whether or not the clause is soft
- block(mcs)#
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.- Parameters
mcs (iterable(int)) – an MCS to block
- compute(enable=[])#
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 caseNone
will be reported as solution. Also, the smallest clause index is assumed to be1
.- Parameters
enable (iterable(int)) – a sequence of clause ids to enable
- Return type
list(int)
- delete()#
Explicit destructor of the internal SAT oracle.
- do_cld_check(cld)#
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.
- 2
Joao Marques-Silva, Federico Heras, Mikolas Janota, Alessandro Previti, Anton Belov. On Computing Minimal Correction Subsets. IJCAI 2013. pp. 615-622
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})\).
- Parameters
cld (list(int)) – clause \(D\) to check
- enumerate()#
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.
- oracle_time()#
Report the total SAT solving time.