Design and Implementation of Exact MAX-SAT Solvers

Jordi Planes Affiliation: Consejo Superior de Investigaciones Científicas. Institut d'Investigació en Intel·ligència Artificial (Bellaterra, España) Biography: Not available Close window

Jordi Planes About the authors  Publication year: 2008 Language: English Subjects: Science and Technology Collection: Monografies de l'Institut d'Investigació en Intel-ligencia Artificial Free eBook

Abstract:

The Propositional Satisfiability Problem (SAT) is the problem of determining whether a truth assignment satisfies a CNF formula. Nowadays, many hard combinatorial problems such as practical verification problems in hardware and software can be solved efficiently by encoding them into SAT. In this thesis, we focus on the Maximum Satisfiability Problem (MAX-SAT), an optimization version of SAT which consists of finding a truth assignment that satisfies the maximum number of clauses in a CNF formula. We also consider a variant of MAX-SAT, called weighted MAX-SAT, in which every clause is associated with a weight and the problem consists of finding a truth assignment in which the sum of weights of violated clauses is minimum. While SAT is NPcomplete and well-suited for encoding and solving decision problems, MAX-SAT and weighted MAX-SAT are NP-hard and well-suited for encoding and solving optimization problems. This thesis is concerned with the design, implementation and evaluation of exact MAX-SAT solvers based on the branch and bound scheme, with special emphasis on defining good quality lower bounds, powerful inference techniques, clever variable selection heuristics and suitable data structures.

Table of Contents (0.06 Mb)

Preview (0.12 Mb)

This book was added to our online catalog on Thursday 31 July, 2014.