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.
>>> frompysat.examples.rc2importRC2>>> frompysat.formulaimportWCNF>>>>>> wcnf=WCNF(from_file='formula.wcnf.xz')>>>>>> withRC2(wcnf)asrc2:... forminrc2.enumerate():... print('model {0} has cost {1}'.format(m,rc2.cost))model [-1, -2, 3] has cost 2model [1, -2, -3] has cost 2model [-1, 2, -3] has cost 2model [-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.
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()),
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
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.
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().
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)
>>> frompysat.examples.rc2importRC2>>> frompysat.formulaimportWCNF>>>>>> 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)>>>>>> withRC2(wcnf)asrc2:... 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
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()).
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.
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
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
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 out unnecessary selectors and sums from the list of
assumption literals. The corresponding values are also
removed from the dictionaries of bounds and weights.
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:
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.
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.
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
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 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 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].
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.
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.
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
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
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.
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).
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().
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.
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.
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:
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.
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.
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.