• PhD Student:
  • Alexis de Colnet
  • Funding : ANR
  • PhD defended on :
  • Sep 26, 2022 • Salle des thèses

The subject of the thesis is knowledge compilation, an approach for computationally hard problems that aims to work around general lower bounds results by preprocessing an input function. The preprocessing generates an equivalent representation of that function in a class of representations called compilation language. We call “size of a function in a compilation language L” the size of the smallest representation in L for that function. A general observation is that compilation languages that are the most efficient to reason on functions are also those in which the size of functions is the largest. Studying the size of particular functions in a compilation language helps understanding for what kind of functions compiling into this language is relevant. In this thesis, we study the different aspects of the compilation language of Boolean circuits in decomposable negation normal form (DNNF). We use and improve the techniques to analyze such circuits to prove exponential lower bounds on the size of circuits in DNNF representing particular functions and even approximations of these functions. We then show applications of these lower bounds both in the domain of knowledge compilation and outside knowledge compilation, in particular in the area of proof complexity theory.

Thesis committee


  • Adnan Darwiche, University of California
  • Stefan Szeider, Technische Universität Wien


  • Sophie Tison, Université de Lille
  • Florent Capelli, Université de Lille


  • Pierre Marquis, Université d’Artois (advisor)
  • Stefan Mengel, CNRS (supervisor)