On solving the partial MAX-SAT problem

Zhaohui Fu, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

164 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationTheory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings
PublisherSpringer Verlag
Pages252-265
Number of pages14
ISBN (Print)3540372067, 9783540372066
DOIs
StatePublished - 2006
Event9th International Conference on Theory and Applications of Satisfiability Testing, SAT 2006 - Seattle, WA, United States
Duration: Aug 12 2006Aug 15 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4121 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other9th International Conference on Theory and Applications of Satisfiability Testing, SAT 2006
CountryUnited States
CitySeattle, WA
Period8/12/068/15/06

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'On solving the partial MAX-SAT problem'. Together they form a unique fingerprint.

Cite this