In front of us stands the PSPACE mountain, the road to its top (the PSPACE-complete problems) is littered with problems of increasing difficulty. After leaving the start, the slope is immediately steep: all problems are NP-hard. No one knows today how to prove that there are (or are not) efficient (i.e. polynomial time) solution algorithms for such problems and all the algorithms existing to date require an exponential execution time in the worst case.
Among the NP-hard problems, the easiest to solve in practice are the NP-complete problems. The SAT problem (deciding the satisfiability of a propositional formula) is one of them. It has long been the object of special attention, which led to the advent of so-called “modern” SAT solvers at the beginning of our millennium. These solvers are currently capable of solving many industrial problems in practice.
This presentation describes our ascent to the top of the PSPACE mountain using such solvers. It first traces our contributions to practical SAT solving. He then explains how to use them to solve in practice harder and harder problems, such as computing maximally consistent sets of propositional formulas, compiling such formulas and counting the number of their models, and concludes with the presentation of a new algorithmic scheme allowing in particular to decide the satisfiability of formulas in modal logic at the top of the PSPACE mountain.
- Pierre Marquis - Professor, CRIL - University of Artois
- Andreas Herzig - Research Director, IRIT - CNRS
- Thomas Schiex - Research Director, INRA Toulouse
- Hélène Fargier - Research Director, IRIT - CNRS
- Philippe Dague - Professor, University of Paris-Sud
- Christine Solnon - Professor, INSA Lyon