(english version follows)
# Soutenance
Si vous avez trouvé cette page, alors vous êtes cordialement invité à venir me voir gesticuler devant un rétro-projecteur afin de présenter ma thèse intitulée ["Structural restrictions of CNF-formulas: applications to model counting and knowledge compilation"](these_capelli.pdf) ou, en gaulois, ["Restrictions structurelles de formules CNF : applications au comptage et à la compilation de connaissances"](these_capelli.pdf). Vous êtes aussi bien entendu chaleureusement invité au pot qui suivra, même si vous n'avez pas eu le courage de venir à l'exposé, qui devrait commencer autour de 13h. Ci-dessous un résumé de ma thèse :
__Résumé__ : Le problème SAT est connu pour être facile sur des instances particulières où la forme des clauses autorisées est restreinte, comme c'est le cas pour 2-SAT ou Horn-SAT. En revanche, le problème de comptage associé, #SAT, est déjà aussi difficile que le cas général pour ces sous-problèmes. On peut toutefois trouver de nombreux cas où ce problème peut être résolu en temps polynomial en restreignant structurellement la formule d'entrée, c'est-à-dire en restreignant la façon dont les variables interagissent avec les clauses.
Dans cette thèse, nous nous intéressons à la question de comprendre quelles sont les restrictions structurelles pertinentes pour ce problème et essayons de déterminer la frontière entre les cas faciles et les cas aussi difficiles que le cas général. Nous introduisons des algorithmes en temps polynomial pour de nouvelles restrictions structurelles. En particulier, nous prouvons que #SAT sur des formules beta-acycliques, une restriction structurelles pour laquelle seule la décision était connue comme étant facile, peut être résolu en temps polynomial. De plus, nous montrons que tous les algorithmes de comptage connus à ce jour pour ces restrictions structurelles peuvent être vus comme des algorithmes de compilation qui transforment une formule CNF en un petit circuit booléen ayant de fortes propriétés permettant une résolution rapide de différents problèmes comme le comptage ou l'énumération.
Enfin, nous nous intéressons aux limites de l'approche par restrictions structurelles en prouvant des bornes inférieures non-polynomiales sur la taille de tels circuits représentant des formules CNF.
## Informations pratiques
__Important :__ *si vous prévoyez de venir non-armé et que vous n'êtes pas de Paris 7, il faut me prévenir pour que je puisse donner votre nom aux vigiles afin qu'ils vous laissent rentrer (même en baskets).*
* __Quand ?__
* 27 Juin 2016
* 11h
* Le pot devrait commencer aux alentours de 13h pour ceux qui ne seraient pas intéressés par la partie scientifique. Il est difficile d'être précis à ce niveau-là étant donné que cela dépend du temps que prendront les questions et la délibération.
* __Où ?__
* [Bâtiment Sophie Germain](http://www.openstreetmap.org/?box=yes&bbox=2.3807551%2C48.8266741%2C2.3817617%2C48.8274472#map=19/48.82706/2.38126)
* Salle 013
* Accès : Tram 3 Avenue de France, Métro 14/RER C Bibliothèque François Mitterand
* __Jury__ :
* [Arnaud Durand](http://www.logique.jussieu.fr/~durand/index.php)
* [Dieter Kratsch](http://www.lita.sciences.univ-metz.fr/~kratsch/)
* [Pierre Marquis](http://www.cril.univ-artois.fr/~marquis/Home,_sweet_home.html)
* [Luc Segoufin](http://pages.saclay.inria.fr/luc.segoufin/)
* [Olivier Serre](https://www.irif.univ-paris-diderot.fr/~serre/index.html)
* [Bruno Zanuttini](https://zanuttini.users.greyc.fr/)
# Defense (English version)
If you have found this page, then you are cordially invited to the defense of my PhD entitled ["Structural restrictions of CNF-formulas: applications to model counting and knowledge compilation"](these_capelli.pdf). You are also naturally invited to the following cocktail. It should start aroud 1 P.M. Here is an abstract of the thesis:
__Abstract__: It is well-known that clause restrictions of CNF-formulas such as 2-SAT or Horn-SAT are easy instances of the problem SAT. It is however not the case for harder problems such as #SAT, the problem of counting the satisfying assignments of a CNF-formula: #2-SAT is already as hard as the general case. Fortunately, structural restrictions of the input formula, that are restrictions on the way the variables interact with the clauses, have been a successful approach to find large classes of formulas for which #SAT is doable in polynomial time.
In this thesis, we investigate the question of understanding the tractability frontier of the problem #SAT. We prove new tractability results, in particular, the tractability of #SAT on beta-acyclic instances, a structural restriction for which only SAT was known to be tractable. Moreover we show that for every tractable class known so far, we can transform the counting algorithm into a compilation algorithm that construct a succinct representation of the input CNF-formula that support many queries in polynomial time such as counting or enumeration.
Finally, we study the theoretical limits of structural restrictions by proving new lower bounds on the size of the such representations of CNF formulas.
## Practical informations
__Important__: *if you plan to come unarmed and are not from Paris 7, you should tell me in advance in order for me to give your name to the security guard. Otherwise, you will not be authorized to enter the building (even if you are well-dressed).*
* __When ?__
* June 27, 2016
* 11 A.M.
* The cocktail shoud start around 1 P.M. but it is hard to tell since it depends on the time allowed for questions.
* __Where ?__
* [Bâtiment Sophie Germain](http://www.openstreetmap.org/?box=yes&bbox=2.3807551%2C48.8266741%2C2.3817617%2C48.8274472#map=19/48.82706/2.38126)
* Room 013
* Access : Tram 3 Avenue de France, Métro 14/RER C Bibliothèque François Mitterand
* __Jury__:
* [Arnaud Durand](http://www.logique.jussieu.fr/~durand/index.php)
* [Dieter Kratsch](http://www.lita.sciences.univ-metz.fr/~kratsch/)
* [Pierre Marquis](http://www.cril.univ-artois.fr/~marquis/Home,_sweet_home.html)
* [Luc Segoufin](http://pages.saclay.inria.fr/luc.segoufin/)
* [Olivier Serre](https://www.irif.univ-paris-diderot.fr/~serre/index.html)
* [Bruno Zanuttini](https://zanuttini.users.greyc.fr/)