Florent Capelli: Structural restrictions of CNF formulas: applications and limitations

PRACTICALITIES

Lunch is served at 12:00 noon (register at this doodle at the latest on Monday March 14, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

ABSTRACT

It is well-known that clauses 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, restrictions on the way the variables interact with the clauses have been a successful approach to find large classes of formulas for which #SAT was doable in polynomial time.

In the first part of this lunch seminar, I will give a broad picture of what can be done with these structural restrictions of CNF formulas. I will first present how such restrictions are defined and give an overview of the tractability results they enable for #SAT. I will then leverage these results to the broader problem of knowledge compilation, that is, the problem of finding a good data structure representing F that supports queries such as model counting or enumeration in polynomial time. This naturally raises the questions of finding hard instances for such algorithmic techniques. We reformulate these questions as proving lower bounds in knowledge compilation and answer this by giving new exponential lower bounds on the compilation of some family of CNF formulas.

In the second and more technical part of the talk, I will either present the algorithmic techniques in more details or give a complete proof of one of the lower bounds mentioned above depending on what the audience prefers. Most of the results presented in this talk were conceived in collaboration with Simone Bova, Stefan Mengel and Friedrich Slivovsky.