Daniel Le Berre: SAT and friends: a single engine for many purposes

Over the last decade, Boolean reasoning engines received a lot of interest: SAT, MAXSAT, Pseudo-Boolean solvers are now used routinely in hardware or software verification, bioinformatics, software engineering, etc. Using so called "incremental SAT solvers", it is currently possible to solve a lot of different problems by encoding everything into SAT. The presentation will focus on the relationship between various problems based on Boolean reasoning such as SAT, MAXSAT, Pseudo-Boolean Optimization, and how they can be solved using a SAT solver. We will focus particularly on the approach taken in the Sat4j library. A real application, software dependency management, will be used through the presentation to illustrate a possible use of each Boolean reasoning task.