Document Type

Technical Report

Publication Date

2004-02-15

Filename

wucse-2004-16.pdf

Technical Report Number

WUCSE-2004-16

Abstract

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 logical formula. A branch-and-bound algorithm based on the Davis-Putnam-Logemann-Loveland procedure (DPLL) is one of the most efficient complete algorithms for solving max-SAT. In this paper, We propose and investigate a number of new strategies for max-SAT. Our first strategy is a set of unit propagation rules for max-SAT. As unit propaga-tion is a very efficient 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.

Comments

Permanent URL: http://dx.doi.org/10.7936/K7BK19QQ

Download

Share

COinS