Research school: An Overview of Knowledge Compilation
Introduction
The complexity of many queries that have to be performed on data is highly dependent on the way it is represented. An easy way to observe this phenomenon is to look at the satisfiability problem: while it is well known that it is hard to decide if a boolean formula is satisfiable in general, it is completely trivial if the input is a truth table. In this example however, it is not hard to realise that the encoding of a boolean function by its truth table is usually much bigger than with a circuit.
The goal of knowledge compilation is to study how the representation of the data may be changed to make many interesting queries such as counting or conditionning easy without blowing up the size of the representation. This has lead both to the introduction of many representation languages having different trade-offs in terms of succinctness and complexity of several interesting queries and to the design of efficient algorithms that can change the representation of the input into a more tractable language.
In this research school, we propose to give an introduction to knowledge compilation by first presenting the different representations people are interested in together with the queries they support. We will then present different preprocessings originating from SAT Solvers that can be used on the data to enhance its compilability. Finally, we will present different compilation algorithms: some of them being very theoretical with guarantees on the size of the produced representation, others having been implemented in real-world tools and using interesting heuristics that we will explain. Some tools will be presented in details during the exercise sessions.
Teachers
- Florent Capelli, Université Lille 3, CRIStAL, LINKS, florent.capelli@univ-lille3.fr
- Jean-Marie Lagniez, Université d’Artois, CRIL, lagniez@cril.fr
- Pierre Marquis, Université d’Artois, CRIL, marquis@cril.univ-artois.fr
Tentative schedule
There will be a 30mn break every morning and a 15mn break every afternoon. All lectures will take place at Amphi B but the one on Friday morning that will take place in Amphi Schrödinger.
- Monday (Amphi B): 8:30-12:00, 13:30-15:45
- Tuesday (Amphi B): 8:30-12:00, 13:30-15:45
- Wednesday (Amphi B): 8:30-12:00, 13:30-15:45
- Thursday (Amphi B): 8:30-12:00
- Friday: 8:30-12:00 (Amphi Schrödinger), 13:30-14:30 (Amphi B)
Content
Monday: What is knowledge compilation? (F. Capelli)
Morning (8:30-12:00):
- General idea of Knowledge compilation
- A theoretical framework to study the compilability.
Afternoon (13:30-15:45):
- The Knowledge Compilation Map.
- Exercise session on the KC Map.
Material:
To learn more on this:
- On branching programs: Wegener, Ingo. Branching programs and binary decision diagrams: theory and applications, 2000.
- On the KC map: Darwiche, Adnan et Marquis, Pierre. A knowledge compilation map, Journal of Artificial Intelligence Research, 2002, vol. 17
Tuesday: SAT solvers and top down compilation (JM. Lagniez, P. Marquis)
Morning (8:30-12:00):
- Presentation of SAT solvers: DPLL vs CDCL.
- KC as the trace of a counting algorithm
- Presentation of Decision-DNNF compilers (c2d, D4)
Afternoon (13:30-15:45):
- Exercise session: modeling of a configuration problem with CNF.
Material:
Wednesday: NP-preprocessing (JM. Lagniez, P. Marquis)
Morning (8:30-12:00):
- Present NP-preprocessing techniques for model counting and compilation.
Afternoon (13:30-15:45):
- Exercise session (bring a laptop with you): compiling the configuration problem of Tuesday.
Material:
Thursday: Compilation of structured CNF formulas (F. Capelli)
Morning (8:30-12:00):
- FPT algorithms.
- Treewidth.
- Graphs associated with CNF formulas.
- Compilation of bounded treewidth formulas.
Afternoon: free!
Material:
To learn more on this:
- Flum, Jörg, and Martin Grohe. Parameterized complexity theory. Springer Science & Business Media, 2006.
Friday: Advanced KC (JM. Lagniez, F. Capelli).
Morning (8:30-12:00):
- Non-conditional lower bounds
- Bottom up algorithms
- New target languages: EADT, MDDG, ADD…
Afternoon (13:30-14:30):
- Test.
Material: