Seminar on Boolean Constraint Reasoning (Autumn 2010)
Constraint reasoning techniques provide generic means for attacking extremely hard combinatorial problems. This approach is based on expressing problems declaratively through mathematical constraints, and using automated tools (constraint solvers) to reason about (find solution to) the problems on the level of the constraints.
Today, state-of-the-art constraint reasoning methods find applications
in various domains, ranging from hardware and software
verification (e.g., in guaranteeing the correctness of processors and
device drivers) and testing to
scheduling, planning, and bioinformatics.
Particularly exciting is the progress seen within the last 10 years
in the development of highly efficient Boolean constraint reasoning techniques,
especially Boolean satisfiability solving methods, SAT solvers.
The aim of the seminar is to provide a summary of state-of-the-art
constraint reasoning techniques, with an emphasis on Boolean
satisfiability (SAT solving) and its extensions. Both theoretical and practical
aspects and applications will be covered based on handbook chapters
complemented with recently published scientific papers.
- Time: Wednesdays 14-16 during study periods I and II - see the
seminar schedule for details
- Place: Exactum, seminar room C220
- Course code: 58310301
- Credit units: 3
- Teacher-in-charge: Dr. Matti Järvisalo,
- Language: The seminar is held by default in English (given that there are participants who do not speak Finnish).
It is also possible to give a presentation / write the report in Finnish (however, English is recommended).
- Material: Selected chapters from Handbook of Satisfiability (A. Biere, M. Heule, H. van Maaren, and T. Walsh, eds.), IOS Press 2009 + selected recently published scientific articles. You do not have to purchase the handbook in order to take the course, copies of the required chapters will be provided by the teacher.
See the list of possible topics for details.
- Prerequisites: You must have passed the course Scientific Writing or have equivalent skills. Otherwise, no formal prerequisites. Courses from the CS curriculum which may provide useful background include
Design and Analysis of Algorithms,
Introduction to Artificial Intelligence,
and Models of Computation.
You will have significant advantage if you have basic knowledge of (propositional) logic,
but this is not a necessity. Most important, however, is a desire to actively learn new things!
- Requirement for passing the course: (i) A seminar presentation (40 minutes), (ii) a report paper (around 10 pages) on a selected topic related to the seminar, (iii) acting as an opponent for another student. You must individually pass all three parts in order to pass the course.
- Preliminary seminar presentation slides and the report paper must be sent to the teacher by email one week (by previous Wednesday) before the seminar presentation.
- You have the opportunity to receive feedback to your slides and report from the teacher already before your presentation. If you want to take advantage of this opportunity, you should contact the teacher to make an appointment.
- The deadline for submitting a final, polished version of your report is one week after your presentation. This gives the possibility for you to revise the report based on feedback given both by the teacher and during the presentation.
- Grading: The presentation (weight 40%) and report paper (weight 40%) are both graded on the scale 1-5. Active participation, including acting as an opponent and actively attending the presentations, also has an influence on the grade (weight 20%).
Keep in mind that the written report and the oral presentation have partially different goals.
The oral presentation should explain the main ideas of the content, simplifying concepts when necessary. Depending on the topic, a good presentation should include many examples to illustrate the subject matter and only some choice technical details that are important and can be discussed thoroughly enough during the presentation. The oral presentation should last 40 minutes (plus discussions).
For the report, put more emphasis on exactness and scientific representation. The report will often be a summary of the source material, so you must pick and choose what to include. The things you have picked to discuss in your report must then be described in enough detail; for the things you leave out, refer to the source material. A suitable length for the report is 10 pages.
- The International Conferences on
Theory and Applications of Satisfiability Testing (SAT)
- The international SAT Competitions
- Some publicly available SAT solvers - for more, consult the webpages of the recent SAT competitions
- CDCL/DPLL solvers: Minisat, Precosat, Lingeling, Rsat, Tinisat, Glucose, Cryptominisat, Clasp, March_dl, ...
- Local search: the UBCSAT solver implements an impressive number of local search methods; UnitWalk, ...
- DPVis: a visualizer for SAT instances and DPLL
||Practical arrangements, short introduction, distribution of topics
ECAI 2010 tutorial
and SAC 2010 tutorial
AAAI 2007 tutorial
||Break in the schedule
||(Students prepare reports and presentations)
||Graph coloring by SAT
Below are listed possible topics for giving a presentation and writing a report. Each student chooses one topic, and one topic can be chosen only by one student. The provided articles for each topic serve as the main references,
but it is a plus if you independently consult additional suitable references.
The topics will be assigned during the first two seminar meetings (introduction to the topic presented by the teacher) on a first-come-first-served basis. You can also reserve a topic before the first meeting by contacting the teacher.
It is also possible suggest a topic outside this list; if you wish to suggest one, please contact the teacher in advance for fixing the details.
Conflict-driven clause learning (CDCL)
- Chapter 4 of Handbook of Satisfiability
- A well-known solver: Niklas Eén, Niklas Sörensson: An Extensible SAT-solver. SAT 2003: 502-518
Stochastic local search (SLS)
- Additionally, knowledge compilation could be considered
- Non-Clausal / Circuit Satisfiability
- Unsatisfiable cores / subformulas
- Parallel SAT solving using computing clusters
- L. Guo, Y. Hamadi, S. Jabbour, and L. Sais: Diversification and Intensification in Parallel SAT Solving, CP 2010 (to appear)
- Youssef Hamadi, Saïd Jabbour, Lakhdar Sais: ManySAT: a Parallel SAT Solver.
Journal on Satisfiability, Boolean Modeling and Computation, 6:245-262 (2009)
- Youssef Hamadi, Saïd Jabbour, Lakhdar Sais: Control-Based Clause Sharing in Parallel SAT Solving. IJCAI 2009: 499-504
- Pseudo-Boolean and cardinality constraints
- Model Counting (#SAT)
- Additionally, Quantified boolean formula (QBF) satisfiability could be considered.
Foundations and theory
- Automated planning
- Haplotype inference
- Combinatorial designs
- Automatic test pattern generation (ATPG)
Synthesizing circuits and finding circuit complexity upper bounds by SAT
- Probabilistic inference by #SAT
- Relative efficiency of CDCL algorithms and Resolution
- Parameterized complexity
- Proof complexity lower bounds for Resolution
- Classic paper: Armin Haken: The Intractability of Resolution. Theor. Comput. Sci. 39: 297-308 (1985)
- Paul Beame, Toniann Pitassi: Simplified and Improved Resolution Lower Bounds. FOCS 1996: 274-282
- Chapters 5.1-5.2 and 5.4 (especially 5.4.1) of P. Colte, E. Kranakis: Boolean Functions and Computation Models, Springer 2002.
- Worst-case upper bounds