Design and Implementation of Exact Max-SAT Solvers

Author: Jordi Planes
University:
Advisor: Chu Min Li, Felip Manyà
Year: 2007
Abstract:

The Propositional Satisfiability Problem (SAT) is the problem of determining whether a truth assignment satisfies a CNF formula. Nowadays, many hard combinatorial problems such as practical verification problems in hardware and software can be solved efficiently by encoding them into SAT. In this thesis, we focus on the Maximum Satisfiability problem (MAX-SAT), an optimization version of SAT which consists of finding a truth assignment that satisfies the maximum number of clauses in a CNF formula. We also consider a variant of MAX-SAT, called weighted MAX-SAT, in which every clause is associated with a weight and the problem consists of finding a truth assignment in which the sum of weights of violated clauses is minimum. While SAT is NP-complete and well-suited for encoding and solving decision problems, MAX-SAT and weighted MAX-SAT are NP-hard and well-suited for encoding and solving optimization problems. This thesis is concerned with the design, implementation and evaluation of exact MAX-SAT solvers based on the branch and bound scheme, with special emphasis on defining good quality lower bounds, powerful inference techniques and suitable data structures. First, we have defined three lower bound computation methods: star rule, UP, and UP enhanced with failed literal detection. All of them compute an underestimation of the number of clauses that will become unsatisfied if a partial assignment is completed. Such an underestimation is the number of disjoint subsets that can be declared insatisfiable by deriving, in polynomial time, a resolution refutation from the clauses in the subset. The star rule considers subsets formed by $n$ unit clauses and an n$-ary clause which is the disjunction of the complementary literals of the literals occurring in the unit clauses; a linear unit refutation can be derived from those clauses. UP detects contradictions via unit propagation and identifies, for every contradiction, a subset of the clauses involved in the unit propagation from which a unit refutation can be derived. UP enhanced with failed literal detection allows to identify subsets from which both unit and non-unit refutations can be derived. Second, we have defined a set of inference rules that transform a MAX-SAT instance $\phi$ into another MAX-SAT instance $\phi'$ in such a way that the number of unsatisfied clauses in $\phi$ is the same as the number of unsatisfied clauses in $\phi'$ for every assignment. All of them can be seen as unit resolution refinements adapted to MAX-SAT. Third, we have incorporated the lower bounds and the inference rules into a branch and bound algorithm in such a way that the computation of the lower bounds and the application of the inference rules is done simultaneously by inspecting the implication graph. As a result, we have developed a MAX-SAT solver, called MaxSatz, which was the best performing solver in the First MAX-SAT Evaluation, which was a co-located event of SAT-2006. Fourth, we have defined extremely efficient lazy data structures for branch and bound MAX-SAT solvers with a static variable ordering. We have incorporated those data structures into a weighted MAX-SAT solver, called Lazy, which implements a lower bound and simple weighted MAX-SAT inference rules. Finally, we have conducted a comprehensive experimental investigation that provides empirical evidence of the good performance profile of the lower bounds, inference rules and data structures introduced. The results for both randomly generated and realistic problems show that the solvers developed in this thesis outperform state-of-the-art MAX-SAT and weighted MAX-SAT solvers on a wide range of instances.