Please use this identifier to cite or link to this item:
Title: On solving the partial MAX-SAT problem
Authors: Fu, Z. 
Malik, S.
Issue Date: 2006
Citation: Fu, Z.,Malik, S. (2006). On solving the partial MAX-SAT problem. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4121 LNCS : 252-265. ScholarBank@NUS Repository.
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 UN SAT 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. © Springer-Verlag Berlin Heidelberg 2006.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISBN: 3540372067
ISSN: 03029743
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

checked on Sep 22, 2022

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.