On solving the partial MAX-SAT problem

Zhaohui Fu, Sharad Malik

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

149 Citations (Scopus)

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
Volume4121 LNCS
ISBN (Print)3540372067, 9783540372066
StatePublished - Jan 1 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

Other

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

Fingerprint

Satisfiability Problem
Partial
Artificial intelligence
Boolean Satisfiability
Design Automation
Binary search
Artificial Intelligence
Optimality
Encoding
Assignment
Eliminate
Optimal Solution
Electronics
Scenarios
Experiments
Experiment
Electronic design automation

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Fu, Z., & Malik, S. (2006). On solving the partial MAX-SAT problem. In Theory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings (Vol. 4121 LNCS, pp. 252-265). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4121 LNCS). Springer Verlag.
Fu, Zhaohui ; Malik, Sharad. / On solving the partial MAX-SAT problem. Theory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings. Vol. 4121 LNCS Springer Verlag, 2006. pp. 252-265 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{a95a7882cd6d4c5ca2838e9c123a5746,
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 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.",
author = "Zhaohui Fu and Sharad Malik",
year = "2006",
month = "1",
day = "1",
language = "English (US)",
isbn = "3540372067",
volume = "4121 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "252--265",
booktitle = "Theory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings",
address = "Germany",

}

Fu, Z & Malik, S 2006, On solving the partial MAX-SAT problem. in Theory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings. vol. 4121 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4121 LNCS, Springer Verlag, pp. 252-265, 9th International Conference on Theory and Applications of Satisfiability Testing, SAT 2006, Seattle, WA, United States, 8/12/06.

On solving the partial MAX-SAT problem. / Fu, Zhaohui; Malik, Sharad.

Theory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings. Vol. 4121 LNCS Springer Verlag, 2006. p. 252-265 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4121 LNCS).

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

TY - GEN

T1 - On solving the partial MAX-SAT problem

AU - Fu, Zhaohui

AU - Malik, Sharad

PY - 2006/1/1

Y1 - 2006/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33749564382&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33749564382&partnerID=8YFLogxK

M3 - Conference contribution

SN - 3540372067

SN - 9783540372066

VL - 4121 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 252

EP - 265

BT - Theory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings

PB - Springer Verlag

ER -

Fu Z, Malik S. On solving the partial MAX-SAT problem. In Theory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings. Vol. 4121 LNCS. Springer Verlag. 2006. p. 252-265. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).