Title
On solving the partial MAX-SAT problem
Abstract
Boolean Satisfiability (SAT) has seen many successful applications in various fields such as Electronic Design Automation and Artificial Intelligence. However, in some cases, it may be required/preferable to use variations of the general SAT problem. In this paper, we consider one important variation, the Partial MAX-SAT problem. Unlike SAT, Partial MAX-SAT has certain constraints (clauses) that are marked as relaxable and the rest are hard, i.e. non-relaxable. The objective is to find a variable assignment that satisfies all non-relaxable clauses together with the maximum number of relaxable ones. We have implemented two solvers for the Partial MAX-SAT problem using a contemporary SAT solver, zChaff. The first approach is a novel diagnosis based algorithm; it iteratively analyzes the UNSAT core of the current SAT instance and eliminates the core through a modification of the problem instance by adding relaxation variables. The second approach is encoding based; it constructs an efficient auxiliary counter that constrains the number of relaxed clauses and supports binary search or linear scan for the optimal solution. Both solvers are complete as they guarantee the optimality of the solution. We discuss the relative strengths and thus applicability of the two solvers for different solution scenarios. Further, we show how both techniques benefit from the persistent learning techniques of incremental SAT. Experiments using practical instances of this problem show significant improvements over the best known solvers.
Year
DOI
Venue
2006
10.1007/11814948_25
SAT
Keywords
Field
DocType
contemporary sat solver,known solvers,current sat instance,optimal solution,problem instance,different solution scenario,partial max-sat,incremental sat,partial max-sat problem,general sat problem,sat solver,boolean satisfiability,binary search,satisfiability,electronic design automation,artificial intelligent
Maximum satisfiability problem,#SAT,Constraint satisfaction,Mathematical optimization,Computer science,Satisfiability,Boolean satisfiability problem,Propositional calculus,Algorithm,Boolean algebra,Binary search algorithm
Conference
Volume
ISSN
ISBN
4121
0302-9743
3-540-37206-7
Citations 
PageRank 
References 
126
4.51
11
Authors
2
Search Limit
100126
Name
Order
Citations
PageRank
Zhaohui Fu128314.28
Sharad Malik27766691.24