• Funding : Artois
  • PhD defended on :
  • Dec 14, 2020

logo spi

Summary

This thesis is about the language of pseudo-Boolean constraints, i.e., conjunctions of linear equations or inequations over Boolean variables, that generalizes the well-known CNF format. Our contribution to the study of this language is twofold. In the first part of the thesis, the language of pseudo-Boolean constraints is investigated from a knowledge representation perspective. It is compared to a number of well-known propositional formats using the criteria considered in the so-called knowledge compilation map pointed out by Darwiche and Marquis. On the one hand, an advantage of using pseudo-Boolean constraints as a representation language over CNF formulae is that they can be far more succinct. On the other hand, unfortunately, more operations of interest are NP-hard when dealing with pseudo-Boolean constraints compared to CNF formulae. As a consequence, it is sometimes preferable to consider CNF encodings (instead of CNF representations) of such constraints. Doing so, the practical efficiency of modern SAT solvers can be leveraged to reason with these encodings. We also investigate the properties of such encodings, and show that bounding their width may drastically reduce their expressivity. One reason for considering pseudo-Boolean constraints instead of CNF formulae is that they allow the use of the cutting planes proof system, which is stronger than the resolution proof system implemented in classical SAT solvers based on CNF. In particular, unsatisfiability proofs that may be exponentially shorter than their resolution counterpart can be derived for some sets of pseudo-Boolean constraints. Thus, from the theory side, pseudo-Boolean solvers, i.e., solvers that use pseudo-Boolean constraints natively instead of encodings, could be more efficient than SAT solvers. However, practical solver implementations fail to keep this promise, and understanding why this is the case is an important issue. As a step in this direction, the second part of this thesis deals with the practical resolution of pseudo-Boolean problems. Several weaknesses of current implementations of pseudo-Boolean solvers are identified and for some of them improvements are proposed. In particular, we show that all rules implemented in pseudo-Boolean solvers may produce irrelevant literals during conflict analysis, i.e., literals that have no effect on the truth value of the constraints in which they appear. This is problematic as such literals lead to the inference of constraints that can be weaker than expected, and in turn to the production of longer unsatisfiability proofs. We point out several approaches to deal with those weak points, such as the use of new weakening strategies, that are designed in such a way that a tradeoff between the size of the derived constraints and their strength is obtained. Those weakening strategies may allow to efficiently eliminate irrelevant literals, at the price of deriving weaker constraints. In addition, we show that a more parsimonious (but inevitable) application of the weakening rule may allow improving the performance of the solver. We also lift many variants of strategies that are classically implemented in SAT solvers to the pseudo-Boolean setting. In particular, branching heuristics and quality measures for learned constraints that are adapted to pseudo-Boolean constraints are presented. We show that a careful choice among those strategies may drastically improve the performance of the solver. All practical approaches described in this thesis have been implemented in the pseudo-Boolean solver Sat4j and are publicly available.

Jury committee

Reviewers:

  • Jakob Nordström, University of Copenhagen (Danemark) & Lund University (Suède)
  • Joao Marques-Silva, ANITI - Université de Toulouse

Members:

  • Nadia Creignou, Aix-Marseille Université
  • Daniel Le Berre, Université d’Artois (advisor)
  • Pierre Marquis, Université d’Artois (co-Advisor)
  • Stefan Mengel, CNRS (supervisor)