Romain Wallon: Pseudo-Boolean Constraints: Reasoning and Compilation

Abstract
Pseudo-Boolean constraints, and their associated cutting-planes proof system, are theoretically more powerful than the usual resolution approach. However, even if pseudo-Boolean solvers benefit from some of the last improvements made in SAT solvers, the practical results are disappointing compared to the promises of the theory.

To try to get a better understanding of this phenomenon, an interesting point of view is to consider pseudo-Boolean constraints as a compilation language.

In propositional logic, the Knowledge Compilation Map proposed by Adnan Darwiche and Pierre Marquis in 2002 enables to find out which compilation language is suitable to represent knowledge according to what is intended to be done with it.

In this talk, we will extend this map by adding the pseudo-Boolean constraints to it, and use these results to try to find ways to improve pseudo-Boolean reasoning.