Sciweavers

AI
2005
Springer

MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability

13 years 9 months ago
MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability
Maximum Boolean satisfiability (max-SAT) is the optimization counterpart of Boolean satisfiability (SAT), in which a variable assignment is sought to satisfy the maximum number of clauses in a Boolean formula. A branch and bound algorithm based on the Davis-Putnam-Logemann-Loveland procedure (DPLL) is one of the most competitive exact algorithms for solving max-SAT. In this paper, we propose and investigate a number of strategies for max-SAT. The first strategy is a set of unit propagation or unit resolution rules for max-SAT. We summarize three existing unit propagation rules and propose a new one based on a nonlinear programming formulation of max-SAT. The second strategy is an effective lower bound based on linear programming (LP). We show that the LP lower bound can be made effective as the number of clauses increases. The third strategy consists of a a binary-clause first rule and a dynamicweighting variable ordering rule, which are motivated by a thorough analysis of two existin...
Zhao Xing, Weixiong Zhang
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2005
Where AI
Authors Zhao Xing, Weixiong Zhang
Comments (0)