Welcome Guest!

Quick Find:  

Advanced Search

Languages: English Español

Valid XHTML 1.0 Transitional ¡CSS Válido! Icono de conformidad con el Nivel Doble-A, 
	de las Directrices de Accesibilidad para el 
	Contenido Web 1.0 del W3C-WAI

Design and Implementation of Exact MAX-SAT Solvers


Design and Implementation of Exact MAX-SAT Solvers
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 Table of Contents (0.06 Mb)

Preview Preview (0.12 Mb)

Bibliographic information

Physical Description : XX, 144 p. : gráf. ; 24 cm

ISBN: 978-84-00-08709-8

Publication: Bellaterra (Spain) : Consejo Superior de Investigaciones Científicas, 2008

Reference CSIC: 11666

Other data: Thesis. University of Lleida (España), 2007

Buy the digital edition at

This eBook is available for free download

Free Downloads

Download eBook Download eBook (3.69 Mb)

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