LSU algorithm for MaxSAT (pysat.examples.lsu
)#
List of classes#
Linear SATUNSAT algorithm for MaxSAT 1. 

LSUlike algorithm extended for 
Module description#
The module implements a prototype of the known LSU/LSUS, e.g. linear (search) SATUNSAT, 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.
 1(1,2,3)
António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, Joao MarquesSilva. Iterative and coreguided MaxSAT solving: A survey and assessment. Constraints 18(4). 2013. pp. 478534
 2(1,2)
Ruben Martins, Saurabh Joshi, Vasco M. Manquinho, Inês Lynce. Incremental Cardinality Constraints for MaxSAT. CP 2014. pp. 531548
The implementation can be used as an executable (the list of available
commandline 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', expect_interrupt=False, verbose=0)#
Linear SATUNSAT 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 (seeSolverNames
for details), and an integer verbosity level. Parameters
formula (
WCNF
) – input MaxSAT formulasolver (str) – name of SAT solver
expect_interrupt (bool) – whether or not an
interrupt()
call is expectedverbose (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 formulamodel (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 (seeclear_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, andFalse
otherwise. Return type
bool
 class examples.lsu.LSUPlus(formula, solver, expect_interrupt=False, verbose=0)#
LSUlike algorithm extended for
WCNFPlus
formulas (usingMinicard
). Parameters
formula (
WCNFPlus
) – input MaxSAT formula in WCNF+ formatexpect_interrupt (bool) – whether or not an
interrupt()
call is expectedverbose (int) – verbosity level