2013-03-15 Encoding and Solving Optimization Problems with MinSAT and MaxSAT

15 mars 2013 -- 14h30, salle des séminaires : Felip Manyà -- CSIC Barcelone
Encoding and Solving Optimization Problems with MinSAT and MaxSAT
SAT offers a competitive framework for solving challenging decision problems in domains as diverse as hardware and software verification,
artificial intelligence, and operations research. In recent years, the success of SAT has led to investigate several extensions of SAT,
including Satisfiability Modulo Theories (SMT), Quantified Boolean Formulas (QBF), Pseudo-Boolean Constraints (PB), Model Counting (MC),
Maximum Satisfiability (MaxSAT), and Minimum Satisfiability (MinSAT).
In this talk we will focus on how MaxSAT and MinSAT can be used to solve NP-hard optimization problems. Firstly, we will define MaxSAT, MinSAT and existing variants of these problems. Secondly, we will give an overview of the most recent solving techniques that have been devised for these problems. Thirdly, we will present how NP-hard problems can be modeled as MaxSAT/MinSAT instances, and in particular how MaxCSP can be encoded into MaxSAT/MinSAT. Fourthly, we will report on empirical results that show that MaxSAT/MinSAT are very competitive on certain optimization problems. Finally, we will point out promising research directions.

Dernière mise à jour le 18/06/2013