Solvers and tools to tackle problems in propositional logic

Daniel Le Berre
Université d'Artois
Friday, 31 January, 2014 - 14:00
Forum C
Thanks to the emergence of very efficient SAT engines, the last decade has seen the  design of new solvers to tackle other problems in propositional logic. It is now possible to  solve boolean optimization problems using either Pseudo-Boolean or MAXSAT solvers. Computing a Minimal Unsatisfiable Subformula (or UNSAT core) is now a routine in several solvers. The aim of this talk is to summarize which kind of propositional problems can now be solved in practice. We will especially focus on problems for which the research community provides a common input format and multiple solvers. The last part of the talk will present a tool which allow to model a problem in a friendly domain specific language and to solve it using a SAT solver.