Fu&Malik MaxSAT algorithm (pysat.examples.fm
)#
List of classes#
A non-incremental implementation of the FM (Fu&Malik, or WMSU1) algorithm. |
Module description#
This module implements a variant of the seminal core-guided MaxSAT algorithm originally proposed by [1] and then improved and modified further in [2] [3] [4] [5]. Namely, the implementation follows the WMSU1 variant [5] of the algorithm extended to the case of weighted partial formulas.
The implementation can be used as an executable (the list of available
command-line options can be shown using fm.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
$ fm.py -c cardn -s glucose3 -vv formula.wcnf.xz
c cost: 1; core sz: 2
c cost: 2; core sz: 3
s OPTIMUM FOUND
o 2
v -1 -2 3 0
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.fm import FM
>>> from pysat.formula import WCNF
>>>
>>> wcnf = WCNF(from_file='formula.wcnf.xz')
>>>
>>> fm = FM(wcnf, verbose=0)
>>> fm.compute() # set of hard clauses should be satisfiable
True
>>> print(fm.cost) # cost of MaxSAT solution should be 2
>>> 2
>>> print(fm.model)
[-1, -2, 3]
Module details#
- class examples.fm.FM(formula, enc=0, solver='m22', verbose=1)#
A non-incremental implementation of the FM (Fu&Malik, or WMSU1) algorithm. The algorithm (see details in [5]) is core-guided, i.e. it solves maximum satisfiability with a series of unsatisfiability oracle calls, each producing an unsatisfiable core. The clauses involved in an unsatisfiable core are relaxed and a new \(\textsf{AtMost1}\) constraint on the corresponding relaxation variables is added to the formula. The process gets a bit more sophisticated in the case of weighted formulas because of the clause weight splitting technique.
The constructor of
FM
objects receives a targetWCNF
MaxSAT formula, an identifier of the cardinality encoding to use, a SAT solver name, and a verbosity level. Note that the algorithm uses thepairwise
(seecard.EncType
) cardinality encoding by default, while the default SAT solver is MiniSat22 (referred to as'm22'
, seeSolverNames
for details). The default verbosity level is1
.- Parameters:
formula (
WCNF
) – input MaxSAT formulaenc (int) – cardinality encoding to use
solver (str) – name of SAT solver
verbose (int) – verbosity level
- _compute()#
This method implements WMSU1 algorithm. The method is essentially a loop, which at each iteration calls the SAT oracle to decide whether the working formula is satisfiable. If it is, the method derives a model (stored in variable
self.model
) and returns. Otherwise, a new unsatisfiable core of the formula is extracted and processed (seetreat_core()
), and the algorithm proceeds.
- compute()#
Compute a MaxSAT solution. First, the method checks whether or not the set of hard clauses is satisfiable. If not, the method returns
False
. Otherwise, add soft clauses to the oracle and call the MaxSAT algorithm (see_compute()
).Note that the soft clauses are added to the oracles after being augmented with additional selector literals. The selectors literals are then used as assumptions when calling the SAT oracle and are needed for extracting unsatisfiable cores.
- delete()#
Explicit destructor of the internal SAT oracle.
- init(with_soft=True)#
The method for the SAT oracle initialization. Since the oracle is is used non-incrementally, it is reinitialized at every iteration of the MaxSAT algorithm (see
reinit()
). An input parameterwith_soft
(False
by default) regulates whether or not the formula’s soft clauses are copied to the oracle.- Parameters:
with_soft (bool) – copy formula’s soft clauses to the oracle or not
- oracle_time()#
Method for calculating and reporting the total SAT solving time.
- reinit()#
This method calls
delete()
andinit()
to reinitialize the internal SAT oracle. This is done at every iteration of the MaxSAT algorithm.
- relax_core()#
Relax and bound the core.
After unsatisfiable core splitting, this method is called. If the core contains only one clause, i.e. this clause cannot be satisfied together with the hard clauses of the formula, the formula gets augmented with the negation of the clause (see
remove_unit_core()
).Otherwise (if the core contains more than one clause), every clause \(c\) of the core is relaxed. This means a new relaxation literal is added to the clause, i.e. \(c\gets c\vee r\), where \(r\) is a fresh (unused) relaxation variable. After the clauses get relaxed, a new cardinality encoding is added to the formula enforcing the sum of the new relaxation variables to be not greater than 1, \(\sum_{c\in\phi}{r\leq 1}\), where \(\phi\) denotes the unsatisfiable core.
- remove_unit_core()#
If an unsatisfiable core contains only one clause \(c\), this method is invoked to add a bunch of new unit size hard clauses. As a result, the SAT oracle gets unit clauses \((\neg{l})\) for all literals \(l\) in clause \(c\).
- split_core(minw)#
Split clauses in the core whenever necessary.
Given a list of soft clauses in an unsatisfiable core, the method is used for splitting clauses whose weights are greater than the minimum weight of the core, i.e. the
minw
value computed intreat_core()
. Each clause \((c\vee\neg{s},w)\), s.t. \(w>minw\) and \(s\) is its selector literal, is split into clauses (1) clause \((c\vee\neg{s}, minw)\) and (2) a residual clause \((c\vee\neg{s}',w-minw)\). Note that the residual clause has a fresh selector literal \(s'\) different from \(s\).- Parameters:
minw (int) – minimum weight of the core
- treat_core()#
Now that the previous SAT call returned UNSAT, a new unsatisfiable core should be extracted and relaxed. Core extraction is done through a call to the
pysat.solvers.Solver.get_core()
method, which returns a subset of the selector literals deemed responsible for unsatisfiability.After the core is extracted, its minimum weight
minw
is computed, i.e. it is the minimum weight among the weights of all soft clauses involved in the core (see [5]). Note that the cost of the MaxSAT solution is incremented byminw
.Clauses that have weight larger than
minw
are split (seesplit_core()
). Afterwards, all clauses of the unsatisfiable core are relaxed (seerelax_core()
).