Bienvenido Invitado!

Búsqueda Rápida:  

Búsqueda Avanzada

Idiomas: 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

Max-SAT Formalisms with Hard and Soft Constraints


Max-SAT Formalisms with Hard and Soft Constraints
Max-SAT Formalisms with Hard and Soft Constraints

Josep Argelich

Filiación: Universitat de Lleida. Departament d’Informàtica i Enginyeria Industrial (Lleida, España)

Biografía: No disponible

Cerrar ventana

Josep Argelich

Acerca de los autores 

Año de publicación: 2009

Idioma: inglés

Materias: Ciencia y Tecnología

Colección: Monografies de l'Institut d'Investigació en Intel-ligencia Artificial

eBook gratuito

Resumen:

In this thesis we investigate Max-SAT formalisms for solving combinatorial optimization problems with hard and soft constraints. Such formalisms incorporate the notion of partiality ; i.e., they contain clauses which are mandatory and clauses (or sets of clauses) which are relaxable. On the one hand, this notion captures the constraints of real problems in a more natural way, and produces more compact encodings. On the other hand, the distinction between mandatory and relaxable clauses has a significant impact on the solving techniques that can be applied in branch and bound solvers. Firstly, we define a new Max-SAT formalism, called Soft-SAT, that deals with a block of hard clauses and several blocks of soft clauses. In this formalism, solving an instance consists in finding a truth assignment that satisfies the hard block of clauses and maximizes the number of satisfied soft blocks. Dealing with blocks of clauses allows to define soft constraints without introducing auxiliary variables, and has positive consequences in the solvers because we can define solving techniques which are local to each block, and make an earlier application of inference rules in which the premises are required to be short. Secondly, we describe the Soft-SAT solvers we have designed and implemented: Soft-SAT-S and Soft-SAT-D. They are original Soft-SAT branch and bound solvers equipped with original lazy data structures, powerful inference techniques, good quality lower bounds, and original variable selection heuristics. The heuristics of Soft-SAT-S are static while the heuristics of Soft-SAT-D are dynamic. The experimental investigation performed on a representative sample of instances provides empirical evidence that Soft-SAT is a very competitive generic problem approach, compared with the state-of-the-art approaches developed in the CSP and SAT communities. Thirdly, we present novel solving techniques for Partial Max-SAT, which is a suitable formalism for encoding and solving combinatorial optimization problems, and that has become a standard in the community. The solving techniques we have developed include new sound inference rules, lower bound computation methods based on unit propagation, clause learning and non-chronological backtracking derived from the analysis of both hard and soft conflicts, and preprocessing techniques based on variable saturation, randomization and restarts. Finally, we describe the Partial Max-SAT solvers we have designed and implemented: PMS and W-MaxSatz. PMS was implemented from scratch, and xix its most important feature is the learning module for hard and soft conflicts. W-MaxSatz was implemented on top of the state-of-the-art Max-SAT solver MaxSatz, and its most important feature is the method for computing lower bounds, which includes the computation of underestimations using unit propagation enhanced with failed literal detection, and the application of sound inference rules. W-MaxSatz also incorporates a hard learning module. The experimental comparison between PMS, W-MaxSatz, and the best performing state-of-the-art Partial Max-SAT solvers, as well as the results of the 2007 Max-SAT Evaluation, provide empirical evidence that both solvers are robust and very competitive.

Ver Índice Ver Índice (0.06 Mb)

Vista previa Vista previa (0.12 Mb)

Información bibliográfica

Descripción física del libro: XXI, 145 p. : gráf. ; 24 cm

ISBN: 978-84-00-08849-1

Publicación: Bellaterra (España) : Consejo Superior de Investigaciones Científicas, 2009

Referencia CSIC: 11742

Otros datos: Tesis. Universidad Autónoma de Barcelona (España), 2008

Adquirir la edición digital en

Este eBook está disponible en descarga gratuita

Descargas gratuitas

Descargar eBook Descargar eBook (1.66 Mb)

Este título está en nuestro catálogo electrónico desde el jueves 17 abril, 2014.