Fu&Malik MaxSAT algorithm (`pysat.examples.fm`)#

List of classes#

`FM`	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 target WCNF MaxSAT formula, an identifier of the cardinality encoding to use, a SAT solver name, and a verbosity level. Note that the algorithm uses the pairwise (see card.EncType) cardinality encoding by default, while the default SAT solver is MiniSat22 (referred to as 'm22', see SolverNames for details). The default verbosity level is 1.

Parameters:

formula (WCNF) – input MaxSAT formula
enc (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 (see treat_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 parameter with_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() and init() 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 in treat_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 by minw.

Clauses that have weight larger than minw are split (see split_core()). Afterwards, all clauses of the unsatisfiable core are relaxed (see relax_core()).

SAT solvers’ API (pysat.solvers)

Hard formula generator (pysat.examples.genhard)