Practical SAT Solving
Carsten Sinz and Tomas Balyo

Introduction


Welcome to the homepage of the "Practical SAT Solving" lecture. The lecture takes place every Tuesday (starting 23. 4. 2019) at 14:00 in room -120. The exercises are every second Thursday (starting 25. 4. 2019) at 14:00 in room -119

This website contains the slides used for the lectures and the homework assignments for the exercises.


Please give us feedback about the lecture at any time during the semester.

Lectures


Slides from 2019

Presented bySlidesContents
1. Tomas Balyo (23.4.2019) lecture1.pdfIntroduction, Encodings, Incremental SAT
2. Carsten Sinz (30.4.2019) lecture2.pdfResolution, 2-SAT
3. Tomas Balyo (7.5.2019) lecture3.pdfHornSAT, SLUR, Encoding techniques
4. Tomas Balyo (14.5.2019) lecture4.pdfPlanning as Sat, DIMSPEC
5. Carsten Sinz (21.5.2019) lecture5.pdfLocal Search, Davis-Putnam, DPLL Algorithm, Efficient UP
6. Carsten Sinz (28.5.2019) lecture6.pdfStalmarck's Method, Advanced DPLL
7. Carsten Sinz (4.6.2019) lecture7.pdfClause Learning, CDCL Algorithm
8. Tomas Balyo (11.6.2019) lecture8.pdfCDCL Heuristics
9. Tomas Balyo (18.6.2019) lecture9.pdfPre/In-processing, Parallel SAT
10. Carsten Sinz (25.6.2019) lecture10.pdfSMT, DPLL(T)
11. Carsten Sinz (2.7.2019) lecture10.pdfQF_BV (slides lecture10.pdf, second part)
12. Tomas Balyo (9.7.2019) lecture12.pdfMaxSAT
13. Carsten Sinz (16.7.2019) lecture13.pdfUpper Bounds, Derandomization, Covering Codes

Slides from 2018

Presented bySlidesContents
1. Tomas Balyo (17.4.2018) lecture1.pdfIntroduction, Encodings, Incremental SAT
2. Tomas Balyo (24.4.2018) lecture2.pdfEncodings, Planning as SAT, DIMSPEC
3. Tomas Balyo (8.5.2018) lecture3.pdfResolution, Local Search, Polynomial Cases
4. Carsten Sinz (15.5.2018) lecture4.pdfMore Encodings, Cardinality Constraints, DPLL
5. Carsten Sinz (22.5.2018) lecture5.pdfLiteral Selection Heuristics, Efficient UP
6. Carsten Sinz (29.5.2018) lecture6.pdfStalmarck's Method, Restarts, Phase Saving
7. Tomas Balyo (5.6.2018) lecture7.pdfClause Learning, CDCL Algorithm
8. Tomas Balyo (12.6.2018) lecture8.pdfCDCL Heuristics, Clause Forgetting, Parallel SAT Solvers
9. Carsten Sinz (26.6.2018) lecture9.pdfSMT, DPLL(T), QF_BV
10. Tomas Balyo (10.7.2018) lecture10.pdfMaxSAT
11. Carsten Sinz (17.7.2018) lecture11.pdfUpper Bounds, Derandomization, Covering Codes

Slides from 2017

Presented bySlidesContents
1. Tomas Balyo (24.4.2017) lecture1.pdfIntroduction, Encodings, Incremental SAT
2. Tomas Balyo (08.5.2017) lecture2.pdfEncodings, Planning as SAT, DIMSPEC
3. Tomas Balyo (15.5.2017) lecture3.pdfResolution, Local Search, Polynomial Cases
4. Carsten Sinz (29.5.2017) lecture4.pdfUpper Bounds, Derandomization, Covering Codes
5. Carsten Sinz (12.06.2017) lecture5.pdfMore encodings, Davis-Putnam, DPLL Algorithm
6. Carsten Sinz (19.06.2017) lecture6.pdfLiteral Selection Heuristics, Efficient UP
7. Carsten Sinz (26.06.2017) lecture7.pdfStalmarck's Method, Advanced DPLL
8. Carsten Sinz (03.07.2017) lecture8.pdfClause Learning, CDCL Algorithm
9. Tomas Balyo (10.07.2017) lecture9.pdfVSIDS heuristics, Clause forgetting, Parallel SAT Solving
10. Tomas Balyo (17.07.2017) lecture10.pdfMaxSAT Solving
11. Carsten Sinz (24.07.2017) lecture11.pdfSatisfiability Modulo Theory (SMT), DPLL(T), QF_BV

Slides from 2016

Presented bySlidesContents
1. Tomas Balyo (18.4.2016) lecture1.pdfIntroduction, Resolution, Polynomial cases
2. Carsten Sinz (25.4.2016) lecture2.pdfEncodings, Tseitin encoding
3. Tomas Balyo (2.5.2016) lecture3.pdfPlanning as SAT, Random SAT
4. Carsten Sinz (9.5.2016) lecture4.pdfLocal Search, DPLL, Stalmarcks Method
5. Tomas Balyo (23.5.2016) lecture5.pdfDecision heuristics, Restarts, 2-watched literals
6. Markus Iser (30.5.2016) lecture6.pdfBackjumping, Implication graphs, Clause learning
7. Carsten Sinz (6.6.2016) lecture7.pdfCDCL details, Visualization, Decomposition
8. Carsten Sinz (13.6.2016) lecture8.pdf1-UIP Clause, Pre/In-processing
9. Tomas Balyo (20.6.2016) lecture9.pdfParallel and Incremental SAT
10. Carsten Sinz (27.6.2016) lecture10.pdfCDCL Proof generation
11. Tomas Balyo (11.7.2016) lecture11.pdfMaxSAT
12. Carsten Sinz (18.7.2016) lecture12.pdfBounded model checking, SMT

Exercises


Homeworks from 2019

Homework set 1due date 9.5.2019a01.pdf
Homework set 2due date 6.6.2019a02.pdf
Homework set 3due date 27.6.2019a03.pdf
Homework set 4due date 11.7.2019a04.pdf
Homework set 5due date 25.7.2019a05.pdf

Homeworks from 2018

Homework set 1due date 3.5.2018a01.pdf
Homework set 2due date 17.5.2018a02.pdf
Homework set 3due date 7.6.2018a03.pdf
Homework set 4due date 28.6.2018a04.pdf
Homework set 5due date 19.7.2018a05.pdf

Homeworks from 2017

Homework set 1due date 11.5.2017a01.pdf
Homework set 2due date 8.6.2017a02.pdf
Homework set 3due date 22.6.2017a03.pdf
Homework set 4due date 6.7.2017a04.pdf
Homework set 5due date 20.7.2017a05.pdf

Homeworks from 2016

Homework set 1due date 12.5.2016ex01.pdf
Homework set 2due date 2.6.2016ex02.pdf
Homework set 3due date 16.6.2016ex03.pdf
Homework set 4due date 30.6.2016ex04.pdf
Homework set 5due date 14.7.2016ex05.pdf

What we did

What we did in Exercise 1 (2018 and 2019)

  • Donwloaded the SAT solver Glucose version 4.1 from the glucose homepage
  • Compiled glucose (by running |make rs" in the /simp subdirectory)
  • Tested glucose on some random cnf formulas and pidgeon hole formulas: generator skript, wiki page
  • We showed a few ways to encode the at most one (AMO) constraint like the binary and ladder encodings.
  • Implemented an ipasir app that prints all the solutions of a formula.
  • Handed out and explained homework set 1

What we did in Exercise 1 (2016 and 2017)

  • Donwloaded the SAT solver Glucose version 3.0 from the glucose homepage
  • Compiled glucose (by running make in the /simp subdirectory)
  • Tested glucose on a small cnf formula in DIMACS cnf format
  • We added a clause (which was the solution negated) to the small formula to obtain another solution
  • We created a scipt to construct a cnf encoding the pidgeon hole principle
  • We showed two ways to encode the at most one (AMO) constraint - the binary and ladder encodings.
  • We looked at the file format of graphs which we want to use to encode graph coloring.

What we did in Exercise (n+1)

  • We looked at the solutions for homework set (n)
  • Handed out and explained homework set (n+1)