Description du sujet de thèse

The aim of proof complexity is two-fold: originally, it was thought as a way of proving P different from NP by showing that there are no short proofs for coNP. To this end, strong proof systems for different problems, in particular SAT, are studied for with the goal of showing that in general there are no short efficiently verifiable proofs for the problem at hand.

A different, more recent direction of proof complexity originates from the observation that many algorithms implicitly generate proofs of correctness, often some form of representation of the run of the algorithm on an instance. Thus understanding the generated proofs allows a better understanding of the considered algorithm and its limitations. Also, this approach is useful for verifying correctness of the output of solvers implementing the algorithm: explicitly writing out the generated proof allows correctness verification with an independent proof checker which, since it is less complex than a complete solver, is nowadays often formally verified. This allows verifying correctness of the output generated by the solver which in turn makes it possible to trust the solver in critical applications. This approach is most developed in SAT-solving for the DRAT proof system and its variants, but there are also similar approaches for pseudo-Boolean solvers, QBF and the propositional counting problem #SAT (among others).

In recent years, proof complexity has seen several applications of data structures from knowledge compilation, which is a field that systematically studies different trade-offs between desired properties of representations of knowledge, often in the form of Boolean functions. The most important of these representations are so-called circuits in decomposable negation normal form (short DNNF) and their various sub-classes. These circuits are known to strongly relate to different approaches of exhaustive search space exploration for Boolean functions. As such, different flavors of DNNF essentially correspond to different algorithms for counting. This observation has led to the introduction of DNNF as a proof format for #SAT in recent years.

The idea of the proposed thesis is to study knowledge compilation in a proof complexity context more widely. Some example questions are the following: which proof systems for #SAT can be seen as DNNF proofs? Can known separations between different classes of DNNF be lifted to proof systems? Which natural restrictions or extensions of DNNF lead to useful proof systems? Beyond counting, which other problems are amenable to an analysis with the help of knowledge compilation techniques? It is known that DNNF can be used in algorithms for QBF and MaxSAT. Does this give a new perspective on these problems? Does it lead to useful algorithms?

The work on this thesis will mostly deal with foundational, theoretical issues. As such, we expect the successful candidate to have a sound basis in discrete math, graphs, propositional logic, and algorithms. Some background in complexity theory would be an advantage. Due to the international supervising team, the working language for the project will be English.

Contexte de travail

The position will be based at the Centre de Recherche en Informatique de Lens (CRIL). CRIL is a laboratory based in Lens, specializing in various aspects of artificial intelligence.

Contraintes et risques

No particular risk.