Seminar (Combinatorial) Algorithms, Spring 2016
In the academic year 20162017 we will not give the seminar. So next time: spring 2018.
previous years
Last year: Thursdays, February 4, 2016 — May 12, 2016; 9:1511: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:1511: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 :).
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 selfcontained 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 memorystick.
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.
name  email  remarks 



Mark van den Bergh



Hanjo Boekhout



Jelco Burger



Evi Gogou



Anne Hommelberg



Simon Klaver



Bert Peters



Arthur van Rooijen



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) 
CookLevin 
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) 
======================= 
===== 
=====

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.
 Donald Knuth's new book, TAoCP Vol 4, Section 7.2.2.2: Satisfiability. See
here [.ps.gz]
 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/9783319092843
 Valeriy Balabanov, Magdalena Widl, JieHong R. Jiang:
QBF Resolution Systems and Their Proof Complexities.
SAT 2014: 154169.
doi: 10.1007/9783319092843_12
 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: 317332.
doi: 10.1007/9783319092843_24
 Anton Belov, Marijn J. H. Heule, Joao MarquesSilva:
MUS Extraction Using Clausal Proofs.
SAT 2014: 4857
doi: 10.1007/9783319092843_5
 Tamir Heyman, Dan Smith, Yogesh Mahajan, Lance Leong, Husam AbuHaimed:
Dominant Controllability Check Using QBFSolver and Netlist Optimizer.
SAT 2014: 22242
doi: 10.1007/9783319092843_18
 Boris Konev, Alexei Lisitsa:
A SAT Attack on the Erdös Discrepancy Conjecture.
SAT 2014: 219226
doi: 10.1007/9783319092843_17
 Sigve Hortemo Sæther, Jan Arne Telle, Martin Vatshelle:
Solving MaxSAT and #SAT on Structured CNF Formulas.
SAT 2014: 1631
doi: 10.1007/9783319092843_3
 Tomohiro Sonobe, Shuya Kondoh, Mary Inaba:
Community Branching for Parallel Portfolio SAT Solvers.
SAT 2014: 188196
doi: 10.1007/9783319092843_14
 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/9783319243184
 Tomás Balyo, Peter Sanders, Carsten Sinz:
HordeSat: A Massively Parallel Portfolio SAT Solve. SAT 2015: 156122.
doi: 10.1007/9783319243184_12
 Armin Biere, Andreas Fröhlich:
Evaluating CDCL Variable Scoring Schemes. SAT 2015: 405422.
doi: 10.1007/9783319243184_29
 Jonathan Kalechstain, Vadim Ryvchin, Nachum Dershowitz:
Hints Revealed. SAT 2015: 7187.
doi: 10.1007/9783319243184_7
 Chanseok Oh:
Between SAT and UNSAT: The Fundamental Difference in CDCL SAT. SAT 2015: 307323.
 Wiki on
CookLevin theorem; and
Satisfiability

Niklas Eén, Niklas Sörensson:
Translating PseudoBoolean Constraints into SAT.
Journal on Satisfiability, Boolean Modeling and Computation 2(14): 126 (2006)
 Sean Weaver, Katrina Ray, Victor Marek, Andrew Mayer, Alden Walker:
Satisfiabilitybased Set Membership Filters.
Journal on Satisfiability, Boolean Modeling and Computation 8, 129148 (2014)
 Niklas Eén, Armin Biere:
Effective Preprocessing in SAT Through Variable and Clause Elimination.
SAT 2005: 6175
 Matti Järvisalo, Armin Biere, Marijn Heule:
Blocked Clause Elimination.
TACAS 2010: 129144
doi: 10.1007/9783642120022_10
 Joao MarquesSilva, Ines Lynce and Sharad Malik:
CDCL Solvers.
Chapter 4 of the Handbook of Satisfiability (2009)
see here
 Marijn Heule, Oliver Kullmann, Siert Wieringa, Armin Biere:
Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads.
Haifa Verification Conference 2011: 5065
doi: 10.1007/9783642341885_8
 Stephen A. Cook:
A short proof of the pigeon hole principle using extended resolution.
ACM SIGACT Volume 8 Issue 4, OctoberDecember 1976 Pages 2832
 Knot Pipatsrisawat, Adnan Darwiche:
On the Power of ClauseLearning SAT Solvers with Restarts.
CP 2009: 654668
doi: 10.1016/j.artint.2010.10.002
 Alfredo Braunstein, Marc Mézard, Riccardo Zecchina:
Survey propagation: An algorithm for satisfiability.
Random Struct. Algorithms 27(2): 201226 (2005)
doi: 10.1002/rsa.20057
February 20, 2017 — http://www.liacs.leidenuniv.nl/~kosterswa/semalg/index.html