Thesis in proof complexity and knowledge compilation (M/F)
New
- FTC PhD student / Offer for thesis
- 36 months
- BAC+5
This offer is available in English version
This offer is open to people with a document recognizing their status as a disabled worker.
Offer at a glance
The Unit
Centre de Recherche en Informatique de Lens
Contract Type
FTC PhD student / Offer for thesis
Working hHours
Full Time
Workplace
62307 LENS
Contract Duration
36 months
Date of Hire
01/10/2026
Remuneration
2300 € gross monthly
Apply Application Deadline : 05 August 2026 23:59
Job Description
Thesis Subject
The aim of proof complexity is two-fold: originally, it was thought as a way of proving that P is 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.
Your Work Environment
The research will take place at the Centre de Recherche en Informatique de Lens. The CRIL is a research lab situated in Lens, specialized in different aspects of artificial intelligence.
Constraints and risks
No particular risks.
Compensation and benefits
Compensation
2300 € gross monthly
Annual leave and RTT
44 jours
Remote Working practice and compensation
Pratique et indemnisation du TT
Transport
Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€
About the offer
| Offer reference | UMR8188-STEMEN-002 |
|---|---|
| CN Section(s) / Research Area | Information sciences: bases of information technology, calculations, algorithms, representations, uses |
About the CNRS
The CNRS is a major player in fundamental research on a global scale. The CNRS is the only French organization active in all scientific fields. Its unique position as a multi-specialist allows it to bring together different disciplines to address the most important challenges of the contemporary world, in connection with the actors of change.
Create your alert
Don't miss any opportunity to find the job that's right for you. Register for free and receive new vacancies directly in your mailbox.