Seminar on Boolean Constraint Reasoning (Autumn 2010)

Introduction

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.

Course Information

• 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, matti.jarvisalocs.helsinki.fi
• 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, Discrete Optimization, 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!

Course Requirements

• 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.
• Deadlines:
  • 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%).

Guidelines

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 report should be formatted according to the general format (cover etc.) used on the Scientific Writing course, example layout
  • Using LaTeX is recommended. LaTeX-templates are available from http://www.cs.helsinki.fi/u/kurhila/tiki_k2007/coursedescription.html (See "Tools to work with").

Interesting Pointers

• The International Conferences on Theory and Applications of Satisfiability Testing (SAT)
  • Proceedings of the SAT conferences
• The international SAT Competitions
  • SAT Race 2010; results
  • SAT Competition 2009: results
• 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

Schedule

Date	Topic(s)	Presenter(s)	Opponent(s)
Sep 8	Practical arrangements, short introduction, distribution of topics See also: J. Marques-Silva's ECAI 2010 tutorial and SAC 2010 tutorial J. Rintanen's AAAI 2007 tutorial	M.J.	-
	Break in the schedule
	(Students prepare reports and presentations)
Nov 3	Topic 1	Martin	Janne
	Topic 6	Niko	Joel R.
Nov 10	Graph coloring by SAT	Joel R.	Joel K.
	Topic 11	Janne	- (informal)
Nov 17	Topic 13	Chen	Helle
	Topic 2 (cancelled)
Nov 24	Topic 4	Helle	Niko
	Topic 9	Preston	Martin
Dec 1	Topic 15	Lokesh	Chen
	Topic 16	Joel K.	Lokesh, Preston

Topics

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.

Algorithms

1. 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
2. Stochastic local search (SLS)
   • Chapter 6 of Handbook of Satisfiability
   • UnitWalk: Edward A. Hirsch, Arist Kojevnikov: UnitWalk: A new SAT solver that uses local search guided by unit clause elimination. Ann. Math. Artif. Intell. 43(1): 91-111 (2005)
   • Survey propagation: Alfredo Braunstein, Riccardo Zecchina: Survey and Belief Propagation on Random K-SAT. SAT 2003: 519-528

• Additionally, knowledge compilation could be considered

Extensions

3. Non-Clausal / Circuit Satisfiability
   • Sections 21.1-21.3 of Handbook of Satisfiability
   • Christian Thiffault, Fahiem Bacchus, Toby Walsh: Solving Non-clausal Formulas with DPLL Search. CP 2004: 663-678
   • More recent circuit solver: Chi-An Wu, Ting-Hao Lin, Chih-Chun Lee, Chung-Yang Huang: QuteSAT: a robust circuit-based SAT solver for complex circuit structure. DATE 2007: 1313-1318
4. Unsatisfiable cores / subformulas
   • Mark H. Liffiton, Maher N. Mneimneh, Inês Lynce, Zaher S. Andraus, João Marques-Silva, Karem A. Sakallah: A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints 14(4): 415-442 (2009)
   • Éric Grégoire, Bertrand Mazure, Cédric Piette: Using local search to find MSSes and MUSes. European Journal of Operational Research 199(3): 640-646 (2009)
   • Chapter 11 of Handbook of Satisfiability (to the extent applicable)
5. Max-SAT
   • Chapter 19 of Handbook of Satisfiability
   • Javier Larrosa, Federico Heras, Simon de Givry: A logical approach to efficient Max-SAT solving. Artif. Intell. 172(2-3):204-233 (2008)
   • MaxSAT solver based on unsat cores: João Marques-Silva, Jordi Planes: Algorithms for Maximum Satisfiability using Unsatisfiable Cores. DATE 2008: 408-413
6. 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
7. Pseudo-Boolean and cardinality constraints
   • Chapter 22 of Handbook of Satisfiability
   • Translating to SAT: Niklas Eén, Niklas Sörensson: Translating Pseudo-Boolean Constraints into SAT. 2(1-4): 1-26 (2006)
8. Model Counting (#SAT)
   • Chapter 20 of Handbook of Satisfiability
   • Exact model counting:
     Tian Sang, Fahiem Bacchus, Paul Beame, Henry A. Kautz, Toniann Pitassi: Combining Component Caching and Clause Learning for Effective Model Counting. SAT 2004
     Tian Sang, Paul Beame, Henry A. Kautz: Heuristics for Fast Exact Model Counting. SAT 2005: 226-240

• Additionally, Quantified boolean formula (QBF) satisfiability could be considered.

Applications

9. Automated planning
   • Chapter 15 of Handbook of Satisfiability
   • Classic paper: Henry A. Kautz, Bart Selman: Planning as Satisfiability. ECAI 1992: 359-363
   • Article related to the handbook chapter: Jussi Rintanen, Keijo Heljanko, Ilkka Niemelä: Planning as satisfiability: parallel plans and algorithms for plan search. Artif. Intell. 170(12-13): 1031-1080 (2006)
10. Haplotype inference
    • Inês Lynce, Ana Graça, João Marques-Silva, Arlindo L. Oliveira: Haplotype Inference with Boolean Constraint Solving: An Overview. ICTAI (1) 2008: 92-100.
    • Ana Graça, João Marques-Silva, Inês Lynce and Arlindo L. Oliveira: Haplotype inference with pseudo-Boolean optimization. Annals of Operations Research, 2010, in press.
11. Combinatorial designs
    • Chapter 17 of Handbook of Satisfiability
    • Codes: Igor Zinovik, Daniel Kroening, Yury Chebiryak: Computing Binary Combinatorial Gray Codes Via Exhaustive Search With SAT Solvers. IEEE Transactions on Information Theory 54(4): 1819-1823 (2008)
    • Van der Waerden Numbers:
      Michael R. Dransfield, Lengning Liu, Victor W. Marek, Miroslaw Truszczynski: Satisfiability and Computing van der Waerden Numbers. Electr. J. Comb. 11(1): (2004)
      P. R. Herwig, M. J. H. Heule, P. M. van Lambalgen, Hans van Maaren: A New Method to Construct Lower Bounds for Van der Waerden Numbers. Electr. J. Comb. 14(1): (2007)
12. Automatic test pattern generation (ATPG)
    • Section 21.4 of Handbook of Satisfiability
    • Classic paper: Tracy Larrabee: Test pattern generation using Boolean satisfiability. IEEE Trans. on CAD of Integrated Circuits and Systems 11(1): 4-15 (1992)
    • Understanding SAT-based ATPG: Mukul R. Prasad, Philip Chong, Kurt Keutzer: Why is Combinational ATPG Efficiently Solvable for Practical VLSI Circuits? J. Electronic Testing 17(6): 509-527 (2001)
13. Synthesizing circuits and finding circuit complexity upper bounds by SAT
    • Kamath, A.P.; Karmarkar, N.K.; Ramakrishnan, K.G.; Resende, M.G.C.: An interior point approach to Boolean vector function synthesis. MSCAS 1993.
    • Giovani Gomez Estrada: A Note on Designing Logical Circuits Using SAT. ICES 2003: 410-421
    • Arist Kojevnikov, Alexander S. Kulikov, Grigory Yaroslavtsev: Finding Efficient Circuits Using SAT-Solvers. SAT 2009: 32-44
    • E. Demenkov, Arist Kojevnikov, Alexander S. Kulikov, Grigory Yaroslavtsev: New upper bounds on the Boolean circuit complexity of symmetric functions. Inf. Process. Lett. 110(7): 264-267 (2010)
14. Probabilistic inference by #SAT
    • Mark Chavira, Adnan Darwiche: On Probabilistic Inference by Weighted Model Counting. Artificial Intelligence, 172(6-7):772-799, 2008.
    • Tian Sang, Paul Beame, Henry A. Kautz: Performing Bayesian Inference by Weighted Model Counting. AAAI 2005: 475-482

Foundations and theory

15. Relative efficiency of CDCL algorithms and Resolution
    • Knot Pipatsrisawat, Adnan Darwiche On the Power of Clause-Learning SAT Solvers as Resolution Engines. Under review, 2010.
      • Shorter version: On the Power of Clause-Learning SAT Solvers with Restarts. CP 2009: 654-668
    • Sections 3.5-3.6 of Handbook of Satisfiability for background
    • Earlier study: Paul Beame, Henry A. Kautz, Ashish Sabharwal: Towards Understanding and Harnessing the Potential of Clause Learning. J. Artif. Intell. Res. (JAIR) 22: 319-351 (2004)
16. Parameterized complexity
    • Chapter 13 of Handbook of Satisfiability
    • Param. complexity of SLS: Stefan Szeider: The Parameterized Complexity of k-Flip Local Search for SAT and MAX SAT. Discrete Optimization, 2010, to appear.
17. 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.
18. Worst-case upper bounds
    • Chapter 12 of Handbook of Satisfiability
    • Evgeny Dantsin, Andreas Goerdt, Edward A. Hirsch, Ravi Kannan, Jon M. Kleinberg, Christos H. Papadimitriou, Prabhakar Raghavan, Uwe Schöning: A deterministic (2-2/(k+1))n algorithm for k-SAT based on local search. Theor. Comput. Sci. 289(1): 69-83 (2002)