Seminar (Combinatorial) Algorithms, Spring 2016

previous years

Last year: Thursdays, February 4, 2016 — May 12, 2016; 9:15-11:00; Room 403, Snellius.
Subject: "Satisfiability". Literature: see below.

Contents | Schedule | Participants | Deliverables | References

The Seminar (Combinatorial) Algorithms is intended for Master students in Computer Science. Lectures are in English.
The seminar is organised by dr. H.J. (Hendrik Jan) Hoogeboom and dr. W.A. (Walter) Kosters.

Dates: Thursday mornings, 9:15-11:00 hours; February 4, 2016 — May 12, 2016. Room 403, Snellius.

This year's subject is "Satisfiability".
In the first half of the semester every student presents a part from the book/papers mentioned above/below. After that students should study recent literature (or later chapters of the book) and present their results. And maybe do some programming ...
Meetings are on a weekly basis. Students can also suggest neighbouring subjects. For a somewhat more detailed list, see below.
Credit points: 6 ECTS. There is no written exam.

Prerequisites: Algorithms, Complexity, Datastructures (all at bachelor's level, see for instance the Dutch course pages Datastructures and Complexity).

Students should register in advance, in December 2015, by personal visit to the organizers (come on, please do this). The number of participants is at most 10 (approximately :).

Contents

Students are supposed to present and discuss papers, during class. The setup depends on the number of participants.
Every student presents two papers, one in each half of the semester. Each presentation takes about 45 minutes, so in a session we have two presentations. Next to the oral presentations (using PDF or PowerPoint slides, with the additional help of the blackboard) ± ten page self-contained essays on the subject must be written (in LaTeX; in English/Dutch). See here for a template. Deadline: one month after the presentation.
Essays should be improved until students and organizers agree on the contents. Students must be present during all sessions, and are supposed to actively take part in the presentations, e.g., ask questions. Some form of peer review will be used. Immediately after each lecture there is a short discussion between students and organizers, where the presentation is evaluated. The first and second meetings are used to make a proper schedule. Every student is supposed to choose and present two subjects, one in the first half and one in the second half of the seminar.
Students should use their own laptop for the presentations. It is wise to also have the slides for the presentation on a memory-stick. A beamer is always available.

Grading The final grade is composed of the four Ps: presentation (2x), paper (2x), participation (including presence) and peer review OR programming.

Schedule

• Thursday February 4, 2016, 9:15, room 403: Introduction.
• February 11: questions, answers, final schedule.
• February 18: no class.

   
  ========== 1st half: ==============

• February 25:
  • Anne (Cook Levin);
  • Arthur (Examples, Knuth TAoCP).
• March 3:
  • Mark (Erdös discrepancy, Konev SAT2014);
  • Hanjo (CDCL, instead of Oh SAT2015 we have chosen J.P. Marques-Silva and K.A. Sakallah, GRASP: A search algorithm for propositional satisfiability, IEEE Transactions on Computers 48 (1999) 506-521).
• March 10:
  • Jelco (MUS Extraction, Belov et al. SAT2014);
  • Bert (Community Branching, Sonobe et al. SAT2014).
• March 17:
  • Evi (Membership Filters, Weaver et al. 2014).
• March 24:
  • Simon (Structured CNF, Saether et al. SAT2014);
  discussion about 2nd half.

   
  ========== 2nd half: ==============

• March 31: no class.
• April 7:
  • Bert (QBF Resulution, Balabanov et al. SAT2014);
  • Hanjo (Everything, Balyo et al. SAT2014).
• April 14:
  • Anne (Hints, Kalechstain et al. SAT2015);
  • Jelco (Scoring schemes, Biere et al. SAT2015).
• April 21:
  • Mark (Monte Carlo, Knuth, p.77-);
  • Arthur (Dominant, Heyman et al. SAT2014).
• April 28:
  • Evi (Cube and conquer, Heule et al. 2011);
  • Simon (HordeSat, Balyo et al. SAT2015).
• May 12: skipped.

Participants

Deliverables

References

1. Donald Knuth's new book, TAoCP Vol 4, Section 7.2.2.2: Satisfiability. See here [.ps.gz]

   ---

2. SAT2014. Theory and Applications of Satisfiability Testing, 17th International Conference, Carsten Sinz, Uwe Egly (Eds.), July 2014, Lecture Notes in Computer Science, Vol. 8561, 2014.
   doi: 10.1007/978-3-319-09284-3
3. Valeriy Balabanov, Magdalena Widl, Jie-Hong R. Jiang: QBF Resolution Systems and Their Proof Complexities. SAT 2014: 154-169.
   doi: 10.1007/978-3-319-09284-3_12
4. Tomás Balyo, Andreas Fröhlich, Marijn J. H. Heule, Armin Biere: Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask). SAT 2014: 317-332.
   doi: 10.1007/978-3-319-09284-3_24
5. Anton Belov, Marijn J. H. Heule, Joao Marques-Silva: MUS Extraction Using Clausal Proofs. SAT 2014: 48-57
   doi: 10.1007/978-3-319-09284-3_5
6. Tamir Heyman, Dan Smith, Yogesh Mahajan, Lance Leong, Husam Abu-Haimed: Dominant Controllability Check Using QBF-Solver and Netlist Optimizer. SAT 2014: 22-242
   doi: 10.1007/978-3-319-09284-3_18
7. Boris Konev, Alexei Lisitsa: A SAT Attack on the Erdös Discrepancy Conjecture. SAT 2014: 219-226
   doi: 10.1007/978-3-319-09284-3_17
8. Sigve Hortemo Sæther, Jan Arne Telle, Martin Vatshelle: Solving MaxSAT and #SAT on Structured CNF Formulas. SAT 2014: 16-31
   doi: 10.1007/978-3-319-09284-3_3
9. Tomohiro Sonobe, Shuya Kondoh, Mary Inaba: Community Branching for Parallel Portfolio SAT Solvers. SAT 2014: 188-196
   doi: 10.1007/978-3-319-09284-3_14

   ---

10. SAT2015. Theory and Applications of Satisfiability Testing, 18th International Conference, Marijn Heule, Sean Weaver (Eds.), September 2015, Lecture Notes in Computer Science, Vol. 9340, 2015.
    doi: 10.1007/978-3-319-24318-4
11. Tomás Balyo, Peter Sanders, Carsten Sinz: HordeSat: A Massively Parallel Portfolio SAT Solve. SAT 2015: 156-122.
    doi: 10.1007/978-3-319-24318-4_12
12. Armin Biere, Andreas Fröhlich: Evaluating CDCL Variable Scoring Schemes. SAT 2015: 405-422.
    doi: 10.1007/978-3-319-24318-4_29
13. Jonathan Kalechstain, Vadim Ryvchin, Nachum Dershowitz: Hints Revealed. SAT 2015: 71-87.
    doi: 10.1007/978-3-319-24318-4_7
14. Chanseok Oh: Between SAT and UNSAT: The Fundamental Difference in CDCL SAT. SAT 2015: 307-323.

    ---

15. Wiki on Cook-Levin theorem; and Satisfiability
16. Niklas Eén, Niklas Sörensson: Translating Pseudo-Boolean Constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2(1-4): 1-26 (2006)
17. Sean Weaver, Katrina Ray, Victor Marek, Andrew Mayer, Alden Walker: Satisfiability-based Set Membership Filters. Journal on Satisfiability, Boolean Modeling and Computation 8, 129-148 (2014)
18. Niklas Eén, Armin Biere: Effective Preprocessing in SAT Through Variable and Clause Elimination. SAT 2005: 61-75
19. Matti Järvisalo, Armin Biere, Marijn Heule: Blocked Clause Elimination. TACAS 2010: 129-144
    doi: 10.1007/978-3-642-12002-2_10
20. Joao Marques-Silva, Ines Lynce and Sharad Malik: CDCL Solvers. Chapter 4 of the Handbook of Satisfiability (2009)
    see here
21. Marijn Heule, Oliver Kullmann, Siert Wieringa, Armin Biere: Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. Haifa Verification Conference 2011: 50-65
    doi: 10.1007/978-3-642-34188-5_8
22. Stephen A. Cook: A short proof of the pigeon hole principle using extended resolution. ACM SIGACT Volume 8 Issue 4, October-December 1976 Pages 28-32
23. Knot Pipatsrisawat, Adnan Darwiche: On the Power of Clause-Learning SAT Solvers with Restarts. CP 2009: 654-668
    doi: 10.1016/j.artint.2010.10.002
24. Alfredo Braunstein, Marc Mézard, Riccardo Zecchina: Survey propagation: An algorithm for satisfiability. Random Struct. Algorithms 27(2): 201-226 (2005)
    doi: 10.1002/rsa.20057

February 20, 2017 — http://www.liacs.leidenuniv.nl/~kosterswa/semalg/index.html