|
|
|
|
|
Advanced Topics in SAT-Solving
|
|
Carsten Sinz - University of Tübingen
|
|
| 27.09.04 - 01.10.04 |
|
|
|
|
| Announcements: |
|
- Course starts on Monday afternoon, 13:15, in Room 6103
- Exercises: Mo (15:15-17:00), Tu (13:15-15:00), We (15:15-17:00), Th, Fr (13:15-15:00)
- Slides and Exercises can be downloaded here.
- I have moved to room 5105.
- A list of course attendees (in PDF format) can be downloaded here.
|
|
|
|
| Course Outline: |
|
| Date |
Time |
Topic |
Details |
| Mo 27.09.04 |
13:15-15:00 |
Introduction to SAT |
DPLL algorithm, stochastic local search |
| Tu 28.09.04 |
10:15-12:00 |
Theoretical aspects |
Upper and lower bounds, tractable subclasses, threshold phenomena |
| We 29.09.04 |
10:15-12:00 |
Advanced implementation techniques |
Efficient unit propagation, clause learning, parallelization |
| Th 30.09.04 |
10:15-12:00 |
Structural analysis |
Graph structure, visualization, 2-clause substructure |
| Fr 01.10.04 |
10:15-12:00 |
Applications |
BMC, planning, product configuration |
|
|
| Literature and References: |
|
- Kleine Büning, Lettmann: Propositional Logic: Deduction and Algorithms. Cambridge University Press, 1999.
- SAT Conference Proceedings, Springer Verlag.
- SATLIB - The Satisfiability Library
- SAT Live!
- Algorithms for the Satisfiability (SAT) Problem: A Survey (Gu, Purdom, Franco, Wah)
|
|
|
|
| Questions and Comments: sinz@informatik.uni-tuebingen.de |
|
|
|
|
|
|
|
|
|
