• HDR Defended on :
  • Jun 15, 2026 • Salle des thèses, faculté des sciences

Abstract

This manuscript reviews the research I have pursued since defending my thesis in 2016. The main focus is to study how ideas and data structures from knowledge compilation, traditionally focusing on propositional logic and AI, can be applied to other fields of computer science.

Chapter 1 provides a broad introduction to knowledge compilation and introduces the main data structures and concepts that will be used throughout the manuscript. It also contains a few folklore results on knowledge compilation that have not, to the best of our knowledge, been explicitly proven in the literature.

Chapter 2 introduces a new data structure for knowledge compilation called Tree Decision Diagram (TDD). It can be seen as a generalization of OBDDs to tree-like ordering. We show that TDDs enjoy many interesting properties, such as the existence of a minimal canonical form that can be computed easily from any given TDD, unlocking a very simple bottom- up compilation algorithm. We use this algorithm to recover results such as the fact that bounded treewidth Boolean circuits can be transformed into FPT size deterministic DNNF circuit and that QBF is tractable on bounded treewidth instances. This new approach gives a new perspective on these results. Both can be explained by the fact that bounded treewidth circuits and QBF instances have a small number of subfunctions when following a well-chosen tree structure.

Chapter 3 reviews my work on using knowledge compilation to certify the output of #SAT solvers. We show how one can slightly modify the output of many #SAT-solvers so that instead of outputting only the number K of models, it outputs a certificate that the input formula has indeed K models. The correctness of the certificate can then be checked independently, improving our trust in the output of such complex software. We draw new connections between our early work on the subject and the MICE proof system and explain how all these proof systems can be seen as a way of syntactically certifying the equivalence between a CNF formula and a DNNF circuit.

Chapter 4 studied generalizations of data structures from knowledge compilation to non- binary domain. We show how they can be applied to represent the set of answers of database queries and how they can be used to rederive existing results. We first revisit the Yannakakis algorithm by casting it as a compilation algorithm and then show that a modified version of Exhaustive DPLL yields similar theoretical results. We show how this new perspective allows us to compile a broader class of queries than the Yannakakis algorithm, in particular the class of conjunctive queries with negation.

Finally, Chapter 5 shows how knowledge compilation ideas can be applied to the field of convex optimization. In this chapter, we focus on the notion of extended formulations, where the goal is to write down a set of linear constraints describing a given polyhedron, possibly over a space having a larger dimension. We define the convex hull of Boolean function f as the polyhedron given by the convex hull of its models, where models are seen as points in $[0,1]^n$.

We show that when f is given as a DNNF circuit C, then its convex hull can be described with O(|C|) linear constraints, providing a new way of automatically derive extended formulations. We apply this result to the Binary Polynomial Optimization problem and recover many existing tractability results using this new connection with knowledge compilation.

Committee

Warrant

  • Pierre Marquis, Professeur, Université d’Artois

Reviewers

  • Gilles Audemard, Université d’Artois
  • Olaf Beyersdorff, Friedrich Schiller University Jena
  • Hubie Chen, King’s College London

Examiners

  • Luce Brotcorne, Inria Lille
  • Bruno Zanuttini, Université de Caen