CLD-like MCS enumerator (pysat.examples.mcsls)#

List of classes#

MCSls

Algorithm BLS for computing MCSes, augmented with "clause \(D\)" calls.

Module description#

This module implements a prototype of a BLS- and CLD-like algorithm for the computation of a minimal correction subset (MCS) and/or MCS enumeration. More concretely, the implementation follows the basic linear search (BLS) for MCS exctraction augmented with clause D (CLD) oracle calls. As a result, the algorithm is not an implementation of the BLS or CLD algorithms as described in [1] but a mixture of both. Note that the corresponding original low-level implementations of both can be found online.

The implementation can be used as an executable (the list of available command-line options can be shown using mcsls.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

$ mcsls.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.mcsls import MCSls
>>> from pysat.formula import WCNF
>>>
>>> wcnf = WCNF(from_file='formula.wcnf.xz')
>>>
>>> mcsls = MCSls(wcnf, use_cld=True, solver_name='g3')
>>> for mcs in mcsls.enumerate():
...     mcsls.block(mcs)
...     print(mcs)
[1, 3]
[2, 3]
[1, 2]

Module details#

class examples.mcsls.MCSls(formula, use_cld=False, solver_name='m22', use_timer=False)#

Algorithm BLS for computing MCSes, augmented with “clause \(D\)” calls. 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 description of the basic linear search (BLS) 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

_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 _overapprox() (the corresponding oracle is made 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 BLS algorithm presented in [1].

Additionally, if MCSls 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\)”.

_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

_overapprox()#

The method extracts a model corresponding to an over-approximation of an MCS, i.e. it is the model of the hard part of the formula (the corresponding oracle call is made in compute()).

Here, the set of selectors is divided into two parts: self.ss_assumps, which is an under-approximation of an MSS (maximal satisfiable subset) and self.setd, which is an over-approximation of the target MCS. Both will be further refined in _compute().

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 MCSls, 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.

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 BLS

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

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\)” [1], 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 MCSls 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.

previous

LSU algorithm for MaxSAT (pysat.examples.lsu)

next

An iterative model enumerator (pysat.examples.models)