An Efficient Algorithm for Maximum Boolean Satisfiability Based on Unit Propagation, Linear Programming, and Dynamic Weighting
Technical Report Number
Maximum Boolean satisﬁability (max-SAT) is the optimization counterpart of Boolean satisﬁability (SAT), in which a variable assignment is sought to satisfy the maximum number of clauses in a logical formula. A branch-and-bound algorithm based on the Davis-Putnam-Logemann-Loveland procedure (DPLL) is one of the most efﬁcient complete algorithms for solving max-SAT. In this paper, We propose and investigate a number of new strategies for max-SAT. Our ﬁrst strategy is a set of unit propagation rules for max-SAT. As unit propaga-tion is a very efﬁcient strategy for SAT, we show that it can be extended to max-SAT, and can greatly improve the performance of an extended DPLL-based algorithm. Our second strategy is an effective lookahead heuristic based on linear programming. We show that the LP heuristic can be made effective as the number of clauses increases. Our third strategy is a dynamic-weight variable ordering, which is based on a thorough analysis of two well-known existing branching rules. Based on the analysis of these strategies, we develop an integrated, constrainedness-sensitive max-SAT solver that is able to dynamically adjust strategies ac-cording to problem characteristics. Our experimental results on random max-SAT and some instances from the SATLIB show that our new solver outperforms most of the existing com-plete max-SAT solvers, with orders of magnitude of improvement in many cases.
Xing, Zhao and Zhang, Weixiong, "An Efficient Algorithm for Maximum Boolean Satisfiability Based on Unit Propagation, Linear Programming, and Dynamic Weighting" Report Number: WUCSE-2004-16 (2004). All Computer Science and Engineering Research.
Permanent URL: http://dx.doi.org/10.7936/K7BK19QQ