LSU algorithm for MaxSAT (pysat.examples.lsu)#

List of classes#

LSU

Linear SAT-UNSAT algorithm for MaxSAT [1].

LSUPlus

LSU-like algorithm extended for WCNFPlus formulas (using Minicard).

Module description#

The module implements a prototype of the known LSU/LSUS, e.g. linear (search) SAT-UNSAT, algorithm for MaxSAT, e.g. see [1]. The implementation is improved by the use of the iterative totalizer encoding [2]. The encoding is used in an incremental fashion, i.e. it is created once and reused as many times as the number of iterations the algorithm makes.

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

$ lsu.py -s glucose3 -m -v formula.wcnf.xz
c formula: 3 vars, 3 hard, 3 soft
o 2
s OPTIMUM FOUND
v -1 -2 3 0
c oracle time: 0.0000

Alternatively, the algorithm can be accessed and invoked through the standard import interface of Python, e.g.

>>> from pysat.examples.lsu import LSU
>>> from pysat.formula import WCNF
>>>
>>> wcnf = WCNF(from_file='formula.wcnf.xz')
>>>
>>> lsu = LSU(wcnf, verbose=0)
>>> lsu.solve()  # set of hard clauses should be satisfiable
True
>>> print(lsu.cost) # cost of MaxSAT solution should be 2
>>> 2
>>> print(lsu.model)
[-1, -2, 3]

Module details#

class examples.lsu.LSU(formula, solver='g4', incr=False, expect_interrupt=False, verbose=0)#

Linear SAT-UNSAT algorithm for MaxSAT [1]. The algorithm can be seen as a series of satisfiability oracle calls refining an upper bound on the MaxSAT cost, followed by one unsatisfiability call, which stops the algorithm. The implementation encodes the sum of all selector literals using the iterative totalizer encoding [2]. At every iteration, the upper bound on the cost is reduced and enforced by adding the corresponding unit size clause to the working formula. No clauses are removed during the execution of the algorithm. As a result, the SAT oracle is used incrementally.

Warning

At this point, LSU supports only unweighted problems.

The constructor receives an input WCNF formula, a name of the SAT solver to use (see SolverNames for details), and an integer verbosity level.

Parameters:

  • formula (WCNF) – input MaxSAT formula

  • solver (str) – name of SAT solver

  • incr (bool) – enable incremental mode of Glucose

  • expect_interrupt (bool) – whether or not an interrupt() call is expected

  • verbose (int) – verbosity level

_assert_lt(cost)#

The method enforces an upper bound on the cost of the MaxSAT solution. This is done by encoding the sum of all soft clause selectors with the use the iterative totalizer encoding, i.e. ITotalizer. Note that the sum is created once, at the beginning. Each of the following calls to this method only enforces the upper bound on the created sum by adding the corresponding unit size clause. Each such clause is added on the fly with no restart of the underlying SAT oracle.

Parameters:

cost (int) – the cost of the next MaxSAT solution is enforced to be lower than this current cost

_get_model_cost(formula, model)#

Given a WCNF formula and a model, the method computes the MaxSAT cost of the model, i.e. the sum of weights of soft clauses that are unsatisfied by the model.

Parameters:

  • formula (WCNF) – an input MaxSAT formula

  • model (list(int)) – a satisfying assignment

Return type:

int

_init(formula)#

SAT oracle initialization. The method creates a new SAT oracle and feeds it with the formula’s hard clauses. Afterwards, all soft clauses of the formula are augmented with selector literals and also added to the solver. The list of all introduced selectors is stored in variable self.sels.

Parameters:

formula (WCNF) – input MaxSAT formula

clear_interrupt()#

Clears an interruption.

delete()#

Explicit destructor of the internal SAT oracle and the ITotalizer object.

found_optimum()#

Checks if the optimum solution was found in a prior call to solve().

Return type:

bool

get_model()#

This method returns a model obtained during a prior satisfiability oracle call made in solve().

Return type:

list(int)

interrupt()#

Interrupt the current execution of LSU’s solve() method. Can be used to enforce time limits using timer objects. The interrupt must be cleared before running the LSU algorithm again (see clear_interrupt()).

oracle_time()#

Method for calculating and reporting the total SAT solving time.

solve()#

Computes a solution to the MaxSAT problem. The method implements the LSU/LSUS algorithm, i.e. it represents a loop, each iteration of which calls a SAT oracle on the working MaxSAT formula and refines the upper bound on the MaxSAT cost until the formula becomes unsatisfiable.

Returns True if the hard part of the MaxSAT formula is satisfiable, i.e. if there is a MaxSAT solution, and False otherwise.

Return type:

bool

class examples.lsu.LSUPlus(formula, solver='g4', incr=False, expect_interrupt=False, verbose=0)#

LSU-like algorithm extended for WCNFPlus formulas (using Minicard).

Parameters:

  • formula (WCNFPlus) – input MaxSAT formula in WCNF+ format

  • expect_interrupt (bool) – whether or not an interrupt() call is expected

  • verbose (int) – verbosity level

_assert_lt(cost)#

Overrides _assert_lt of LSU in order to use Minicard’s native support for cardinality constraints

Parameters:

cost (int) – the cost of the next MaxSAT solution is enforced to be lower than this current cost

previous

LBX-like MCS enumerator (pysat.examples.lbx)

next

CLD-like MCS enumerator (pysat.examples.mcsls)