Logo

Seminar (Combinatorial) Algorithms, Spring 2016

In the academic year 2016-2017 we will not give the seminar. So next time: spring 2018.

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

In this seminar we will discuss several issues dealing with algorithms, as described in the papers mentioned above.

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

Participants

nameemailremarks
Mark van den Bergh
Hanjo Boekhout
Jelco Burger
Evi Gogou
Anne Hommelberg
Simon Klaver
Bert Peters
Arthur van Rooijen

Deliverables

The table below shows the progress of the submitted papers; this is also visualized in the graph to the right (thanks to Leon for the Python script).
 
subject                                                who        remarks                        
Erdös            Mark first version handed in (4.4) and checked by W (6.4); second version handed in (8.5) and checked by HJ (20.2); final version handed in (3.19)
Cook-Levin Anne first version handed in (7.4) and checked by W (15.4); second version handed in (21.4) and checked by HJ (18.5); final version handed in (20.6)
CDCL Hanjo first version handed in (1.14) and checked by W (2.14); second version handed in (3.14) and checked by HJ (23.14); final version handed in (24.14)
======================= ===== =====
Monte Carlo Mark first version handed in (16.5) and checked by W (18.5); second version handed in (26.17) and checked by HJ (30.18); final version handed in (3.19)
Hints Anne first version handed in (5.7) and checked by W (6.7); second version handed in (13.7) and checked by HJ (21.12); final version handed in (8.14)
Blocked sets Hanjo first version handed in (13.19) and checked by W (17.19)
======================= ===== =====

References

Further references are either books or papers, see below. Books are usually available in room 159/162. Remember that most doi's can only be used from computers within the university domain. Many other books and the internet may be helpful. Special thanks to Marijn Heule for his help.
  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