RC2 MaxSAT solver (pysat.examples.rc2
)#
List of classes#
Implementation of the basic RC2 algorithm. |
|
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.
- 1(1,2,3,4)
António Morgado, Carmine Dodaro, Joao Marques-Silva. Core-Guided MaxSAT with Soft Cardinality Constraints. CP 2014. pp. 564-573
- 2(1,2)
António Morgado, Alexey Ignatiev, Joao Marques-Silva. MSCG: Robust Core-Guided MaxSAT Solving. JSAT 9. 2014. pp. 129-134
- 3
Alexey Ignatiev, António Morgado, Joao Marques-Silva. RC2: A Python-based MaxSAT Solver. MaxSAT Evaluation 2018. p. 22
- 4
Alexey Ignatiev, António Morgado, Joao Marques-Silva. RC2: An Efficient MaxSAT Solver. MaxSAT Evaluation 2018. JSAT 11. 2019. pp. 53-64
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
.
- 5(1,2)
Joao Marques-Silva, Josep Argelich, Ana Graça, Inês Lynce. Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell. 62(3-4). 2011. pp. 317-343
- 6(1,2,3)
Carlos Ansótegui, Maria Luisa Bonet, Joel Gabàs, Jordi Levy. Improving WPM2 for (Weighted) Partial MaxSAT. CP 2013. pp. 117-132
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 includeunsatisfiable 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 isg3
(seeSolverNames
). Additionally, if Glucose is chosen, theincr
parameter controls whether to use the incremental mode of Glucose 7 (turned off by default). Boolean parametersadapt
,exhaust
, andminz
control whether or to apply detection and adaptation of intrinsic AtMost1 constraints, core exhaustion, and core reduction. Unsatisfiable cores can be trimmed if thetrim
parameter is set to a non-zero integer. Finally, verbosity level can be set using theverbose
parameter.- 7(1,2)
Gilles Audemard, Jean-Marie Lagniez, Laurent Simon. Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction. SAT 2013. pp. 309-317
- Parameters
formula (
WCNFPlus
) – (weighted) (partial) CNFPlus formulasolver (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 parameterweight
is set toNone
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 callingenumerate()
).- 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()
andprocess_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 parameterbound
, which is set to1
by default.- Parameters
bound (int) – right-hand side for the sum to be created
- Return type
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 to1
. To block MCSes, set it to-1
. By the default (for blocking MaxSAT models),block
is set to0
.- 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()
, andprocess_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 inself.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 inputWCNFPlus
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 formulaincr (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 byself.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 inam1
. The weight of the new soft clause is set toself.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 selectorsself.core_sels
and sum assumptions involved in the core are treated separately of each other. This is handled by calling methodsprocess_sels()
andprocess_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 infilter_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 infilter_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 sumrhs (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 ofRC2
with two heuristics, namelyBoolean 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 ofRC2
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()
andprocess_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 callingnext_level()
and finished by callingfinish_level()
. Each new optimization level activates more soft clauses by invokingactivate_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.