RC2 MaxSAT solver (`pysat.examples.rc2`)#

List of classes#

`RC2`	Implementation of the basic RC2 algorithm.
`RC2Stratified`	RC2 augmented with BLO and stratification techniques.

Module description#

An implementation of the RC2 algorithm for solving maximum satisfiability. RC2 stands for relaxable cardinality constraints (alternatively, soft cardinality constraints) and represents an improved version of the OLLITI algorithm, which was described in [1] and [2] and originally implemented in the MSCG MaxSAT solver.

Initially, this solver was supposed to serve as an example of a possible PySAT usage illustrating how a state-of-the-art MaxSAT algorithm could be implemented in Python and still be efficient. It participated in the MaxSAT Evaluations 2018 and 2019 where, surprisingly, it was ranked first in two complete categories: unweighted and weighted. A brief solver description can be found in [3]. A more detailed solver description can be found in [4].

The file implements two classes: RC2 and RC2Stratified. The former class is the basic implementation of the algorithm, which can be applied to a MaxSAT formula in the WCNFPlus format. The latter class additionally implements Boolean lexicographic optimization (BLO) [5] and stratification [6] on top of RC2.

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

$ rc2.py -vv formula.wcnf.xz
c formula: 3 vars, 3 hard, 3 soft
c cost: 1; core sz: 2; soft sz: 2
c cost: 2; core sz: 2; soft sz: 1
s OPTIMUM FOUND
o 2
v -1 -2 3
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.rc2 import RC2
>>> from pysat.formula import WCNF
>>>
>>> wcnf = WCNF(from_file='formula.wcnf.xz')
>>>
>>> with RC2(wcnf) as rc2:
...     for m in rc2.enumerate():
...         print('model {0} has cost {1}'.format(m, rc2.cost))
model [-1, -2, 3] has cost 2
model [1, -2, -3] has cost 2
model [-1, 2, -3] has cost 2
model [-1, -2, -3] has cost 3

As can be seen in the example above, the solver can be instructed either to compute one MaxSAT solution of an input formula, or to enumerate a given number (or all) of its top MaxSAT solutions.

Module details#

class examples.rc2.RC2(formula, solver='g3', adapt=False, exhaust=False, incr=False, minz=False, trim=0, verbose=0)#

Implementation of the basic RC2 algorithm. Given a (weighted) (partial) CNF formula, i.e. formula in the WCNFPlus format, this class can be used to compute a given number of MaxSAT solutions for the input formula. RC2 roughly follows the implementation of algorithm OLLITI [1] [2] of MSCG and applies a few heuristics on top of it. These include

unsatisfiable core exhaustion (see method exhaust_core()),
unsatisfiable core reduction (see method minimize_core()),
intrinsic AtMost1 constraints (see method adapt_am1()).

RC2 can use any SAT solver available in PySAT. The default SAT solver to use is g3 (see SolverNames). Additionally, if Glucose is chosen, the incr parameter controls whether to use the incremental mode of Glucose [7] (turned off by default). Boolean parameters adapt, exhaust, and minz control whether or to apply detection and adaptation of intrinsic AtMost1 constraints, core exhaustion, and core reduction. Unsatisfiable cores can be trimmed if the trim parameter is set to a non-zero integer. Finally, verbosity level can be set using the verbose parameter.

Parameters:

formula (WCNFPlus) – (weighted) (partial) CNFPlus formula
solver (str) – SAT oracle name
adapt (bool) – detect and adapt intrinsic AtMost1 constraints
exhaust (bool) – do core exhaustion
incr (bool) – use incremental mode of Glucose
minz (bool) – do heuristic core reduction
trim (int) – do core trimming at most this number of times
verbose (int) – verbosity level

_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

adapt_am1()#

Detect and adapt intrinsic AtMost1 constraints. Assume there is a subset of soft clauses \(\mathcal{S}'\subseteq \mathcal{S}\) s.t. \(\sum_{c\in\mathcal{S}'}{c\leq 1}\), i.e. at most one of the clauses of \(\mathcal{S}'\) can be satisfied.

Each AtMost1 relationship between the soft clauses can be detected in the following way. The method traverses all soft clauses of the formula one by one, sets one respective selector literal to true and checks whether some other soft clauses are forced to be false. This is checked by testing if selectors for other soft clauses are unit-propagated to be false. Note that this method for detection of AtMost1 constraints is incomplete, because in general unit propagation does not suffice to test whether or not \(\mathcal{F}\wedge l_i\models \neg{l_j}\).

Each intrinsic AtMost1 constraint detected this way is handled by calling process_am1().

add_clause(clause, weight=None)#

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 RC2, adding clauses may be helpful when enumerating MaxSAT solutions 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 integer parameter weight can be set to meaning the the clause being added is soft having the corresponding weight (note that parameter weight is set to None by default meaning that the clause is hard).

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
weight (int) – weight of the clause (if any)

>>> from pysat.examples.rc2 import RC2
>>> from pysat.formula import WCNF
>>>
>>> wcnf = WCNF()
>>> wcnf.append([-1, -2])  # adding hard clauses
>>> wcnf.append([-1, -3])
>>>
>>> wcnf.append([1], weight=1)  # adding soft clauses
>>> wcnf.append([2], weight=1)
>>> wcnf.append([3], weight=1)
>>>
>>> with RC2(wcnf) as rc2:
...     rc2.compute()  # solving the MaxSAT problem
[-1, 2, 3]
...     print(rc2.cost)
1
...     rc2.add_clause([-2, -3])  # adding one more hard clause
...     rc2.compute()  # computing another model
[-1, -2, 3]
...     print(rc2.cost)
2

compute()#

This method can be used for computing one MaxSAT solution, i.e. for computing an assignment satisfying all hard clauses of the input formula and maximizing the sum of weights of satisfied soft clauses. It is a wrapper for the internal compute_() method, which does the job, followed by the model extraction.

Note that the method returns None if no MaxSAT model exists. The method can be called multiple times, each being followed by blocking the last model. This way one can enumerate top-\(k\) MaxSAT solutions (this can also be done by calling enumerate()).

Returns:: a MaxSAT model
Return type:: list(int)

>>> from pysat.examples.rc2 import RC2
>>> from pysat.formula import WCNF
>>>
>>> rc2 = RC2(WCNF())  # passing an empty WCNF() formula
>>> rc2.add_clause([-1, -2])
>>> rc2.add_clause([-1, -3])
>>> rc2.add_clause([-2, -3])
>>>
>>> rc2.add_clause([1], weight=1)
>>> rc2.add_clause([2], weight=1)
>>> rc2.add_clause([3], weight=1)
>>>
>>> model = rc2.compute()
>>> print(model)
[-1, -2, 3]
>>> print(rc2.cost)
2
>>> rc2.delete()

compute_()#

Main core-guided loop, which iteratively calls a SAT oracle, extracts a new unsatisfiable core and processes it. The loop finishes as soon as a satisfiable formula is obtained. If specified in the command line, the method additionally calls adapt_am1() to detect and adapt intrinsic AtMost1 constraints before executing the loop.

Return type:: bool

create_sum(bound=1)#

Create a totalizer object encoding a cardinality constraint on the new list of relaxation literals obtained in process_sels() and process_sums(). The clauses encoding the sum of the relaxation literals are added to the SAT oracle. The sum of the totalizer object is encoded up to the value of the input parameter bound, which is set to 1 by default.

Parameters:: bound (int) – right-hand side for the sum to be created
Return type:: ITotalizer

Note that if Minicard is used as a SAT oracle, native cardinality constraints are used instead of ITotalizer.

delete()#: Explicit destructor of the internal SAT oracle and all the totalizer objects creating during the solving process.

enumerate(block=0)#

Enumerate top MaxSAT solutions (from best to worst). The method works as a generator, which iteratively calls compute() to compute a MaxSAT model, blocks it internally and returns it.

An optional parameter can be used to enforce computation of MaxSAT models corresponding to different maximal satisfiable subsets (MSSes) or minimal correction subsets (MCSes). To block MSSes, one should set the block parameter to 1. To block MCSes, set it to -1. By the default (for blocking MaxSAT models), block is set to 0.

Parameters:: block (int) – preferred way to block solutions when enumerating
Returns:: a MaxSAT model
Return type:: list(int)

>>> from pysat.examples.rc2 import RC2
>>> from pysat.formula import WCNF
>>>
>>> rc2 = RC2(WCNF())  # passing an empty WCNF() formula
>>> rc2.add_clause([-1, -2])  # adding clauses "on the fly"
>>> rc2.add_clause([-1, -3])
>>> rc2.add_clause([-2, -3])
>>>
>>> rc2.add_clause([1], weight=1)
>>> rc2.add_clause([2], weight=1)
>>> rc2.add_clause([3], weight=1)
>>>
>>> for model in rc2.enumerate():
...     print(model, rc2.cost)
[-1, -2, 3] 2
[1, -2, -3] 2
[-1, 2, -3] 2
[-1, -2, -3] 3
>>> rc2.delete()

exhaust_core(tobj)#

Exhaust core by increasing its bound as much as possible. Core exhaustion was originally referred to as cover optimization in [6].

Given a totalizer object tobj representing a sum of some relaxation variables \(r\in R\) that augment soft clauses \(\mathcal{C}_r\), the idea is to increase the right-hand side of the sum (which is equal to 1 by default) as much as possible, reaching a value \(k\) s.t. formula \(\mathcal{H}\wedge\mathcal{C}_r\wedge(\sum_{r\in R}{r\leq k})\) is still unsatisfiable while increasing it further makes the formula satisfiable (here \(\mathcal{H}\) denotes the hard part of the formula).

The rationale is that calling an oracle incrementally on a series of slightly modified formulas focusing only on the recently computed unsatisfiable core and disregarding the rest of the formula may be practically effective.

filter_assumps()#

Filter out unnecessary selectors and sums from the list of assumption literals. The corresponding values are also removed from the dictionaries of bounds and weights.

Note that assumptions marked as garbage are collected in the core processing methods, i.e. in process_core(), process_sels(), and process_sums().

get_core()#

Extract unsatisfiable core. The result of the procedure is stored in variable self.core. If necessary, core trimming and also heuristic core reduction is applied depending on the command-line options. A minimum weight of the core is computed and stored in self.minw. Finally, the core is divided into two parts:

clause selectors (self.core_sels),
sum assumptions (self.core_sums).

init(formula, incr=False)#

Initialize the internal SAT oracle. The oracle is used incrementally and so it is initialized only once when constructing an object of class RC2. Given an input WCNFPlus formula, the method bootstraps the oracle with its hard clauses. It also augments the soft clauses with “fresh” selectors and adds them to the oracle afterwards.

Optional input parameter incr (False by default) regulates whether or not Glucose’s incremental mode [7] is turned on.

Parameters:

formula (WCNFPlus) – input formula
incr (bool) – apply incremental mode of Glucose

minimize_core()#

Reduce a previously extracted core and compute an over-approximation of an MUS. This is done using the simple deletion-based MUS extraction algorithm.

The idea is to try to deactivate soft clauses of the unsatisfiable core one by one while checking if the remaining soft clauses together with the hard part of the formula are unsatisfiable. Clauses that are necessary for preserving unsatisfiability comprise an MUS of the input formula (it is contained in the given unsatisfiable core) and are reported as a result of the procedure.

During this core minimization procedure, all SAT calls are dropped after obtaining 1000 conflicts.

oracle_time()#: Report the total SAT solving time.

process_am1(am1)#

Process an AtMost1 relation detected by adapt_am1(). Note that given a set of soft clauses \(\mathcal{S}'\) at most one of which can be satisfied, one can immediately conclude that the formula has cost at least \(|\mathcal{S}'|-1\) (assuming unweighted MaxSAT). Furthermore, it is safe to replace all clauses of \(\mathcal{S}'\) with a single soft clause \(\sum_{c\in\mathcal{S}'}{c}\).

Here, input parameter am1 plays the role of subset \(\mathcal{S}'\) mentioned above. The procedure bumps the MaxSAT cost by self.minw * (len(am1) - 1).

All soft clauses involved in am1 are replaced by a single soft clause, which is a disjunction of the selectors of clauses in am1. The weight of the new soft clause is set to self.minw.

Parameters:: am1 (list(int)) – a list of selectors connected by an AtMost1 constraint

process_core()#: The method deals with a core found previously in get_core(). Clause selectors self.core_sels and sum assumptions involved in the core are treated separately of each other. This is handled by calling methods process_sels() and process_sums(), respectively. Whenever necessary, both methods relax the core literals, which is followed by creating a new totalizer object encoding the sum of the new relaxation variables. The totalizer object can be “exhausted” depending on the option.

process_sels()#

Process soft clause selectors participating in a new core. The negation \(\neg{s}\) of each selector literal \(s\) participating in the unsatisfiable core is added to the list of relaxation literals, which will be later used to create a new totalizer object in create_sum().

If the weight associated with a selector is equal to the minimal weight of the core, e.g. self.minw, the selector is marked as garbage and will be removed in filter_assumps(). Otherwise, the clause is split as described in [1].

process_sums()#

Process cardinality sums participating in a new core. Whenever necessary, some of the sum assumptions are removed or split (depending on the value of self.minw). Deleted sums are marked as garbage and are dealt with in filter_assumps().

In some cases, the process involves updating the right-hand sides of the existing cardinality sums (see the call to update_sum()). The overall procedure is detailed in [1].

set_bound(tobj, rhs, weight=None)#

Given a totalizer sum, its right-hand side to be enforced, and a weight, the method creates a new sum assumption literal, which will be used in the following SAT oracle calls. If weight is left unspecified, the current core’s weight, i.e. self.minw, is used.

Parameters:

tobj (ITotalizer) – totalizer sum
rhs (int) – right-hand side
weight (int) – numeric weight of the assumption

trim_core()#: This method trims a previously extracted unsatisfiable core at most a given number of times. If a fixed point is reached before that, the method returns.

update_sum(assump)#

The method is used to increase the bound for a given totalizer sum. The totalizer object is identified by the input parameter assump, which is an assumption literal associated with the totalizer object.

The method increases the bound for the totalizer sum, which involves adding the corresponding new clauses to the internal SAT oracle.

The method returns the totalizer object followed by the new bound obtained.

Parameters:: assump (int) – assumption literal associated with the sum
Return type:: ITotalizer, int

Note that if Minicard is used as a SAT oracle, native cardinality constraints are used instead of ITotalizer.

class examples.rc2.RC2Stratified(formula, solver='g3', adapt=False, blo='div', exhaust=False, incr=False, minz=False, nohard=False, trim=0, verbose=0)#

RC2 augmented with BLO and stratification techniques. Although class RC2 can deal with weighted formulas, there are situations when it is necessary to apply additional heuristics to improve the performance of the solver on weighted MaxSAT formulas. This class extends capabilities of RC2 with two heuristics, namely

Boolean lexicographic optimization (BLO) [5]
diversity-based stratification [6]
cluster-based stratification

To specify which heuristics to apply, a user can assign the blo parameter to one of the values (by default it is set to 'div'):

'basic' (‘BLO’ only)
div (‘BLO’ + diversity-based stratification)
cluster (‘BLO’ + cluster-based stratification)
full (‘BLO’ + diversity- + cluster-based stratification)

Except for the aforementioned additional techniques, every other component of the solver remains as in the base class RC2. Therefore, a user is referred to the documentation of RC2 for details.

activate_clauses(beg)#: This method is used for activating the clauses that belong to optimization levels up to the newly computed level. It also reactivates previously deactivated clauses (see process_sels() and process_sums() for details).

compute()#: This method solves the MaxSAT problem iteratively. Each optimization level is tackled the standard way, i.e. by calling compute_(). A new level is started by calling next_level() and finished by calling finish_level(). Each new optimization level activates more soft clauses by invoking activate_clauses().

finish_level()#: This method does postprocessing of the current optimization level after it is solved. This includes hardening some of the soft clauses (depending on their remaining weights) and also garbage collection.

init_wstr()#: Compute and initialize optimization levels for BLO and stratification. This method is invoked once, from the constructor of an object of RC2Stratified. Given the weights of the soft clauses, the method divides the MaxSAT problem into several optimization levels.

next_level()#

Compute the next optimization level (starting from the current one). The procedure represents a loop, each iteration of which checks whether or not one of the conditions holds:

partial BLO condition
diversity-based stratification condition
cluster-based stratification condition

If any of these holds, the loop stops.

process_am1(am1)#: Due to the solving process involving multiple optimization levels to be treated individually, new soft clauses for the detected intrinsic AtMost1 constraints should be remembered. The method is a slightly modified version of the base method RC2.process_am1() taking care of this.

process_sels()#: A redefined version of RC2.process_sels(). The only modification affects the clauses whose weight after splitting becomes less than the weight of the current optimization level. Such clauses are deactivated and to be reactivated at a later stage.

process_sums()#: A redefined version of RC2.process_sums(). The only modification affects the clauses whose weight after splitting becomes less than the weight of the current optimization level. Such clauses are deactivated and to be reactivated at a later stage.

OptUx optimal MUS enumerator (pysat.examples.optux)

ApproxMC model counter (pysat.allies.approxmc)

RC2 MaxSAT solver (pysat.examples.rc2)#

List of classes#

Module description#

Module details#

RC2 MaxSAT solver (`pysat.examples.rc2`)#