Max-SAT Formalisms with Hard and Soft Constraints

Josep Argelich Affiliation: Universitat de Lleida. Departament d’Informàtica i Enginyeria Industrial (Lleida, España) Biography: Not available Close window

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

Abstract:

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.

Table of Contents (0.06 Mb)

Preview (0.12 Mb)

This book was added to our online catalog on Thursday 17 April, 2014.