This year INF 339 is on Satisfiability (SAT) problem,
applications and related topics. There will be joint lectures with
INF 349 (advanced topics in cryptography). The main topics are
- Why SAT?
(Place of the SAT( k-SAT) problem in the Theory of
- Main theoretic ideas behind SAT solvers
Describing symmetric ciphers with k-SAT instances,
cryptanalytic algebraic attacks via solving SAT problems.
k-SAT and graph theoretic problems. 2-SAT and MAX-CUT.
Matrix multiplication and exponential algorithms. Constraint
Satisfaction problems (CSP).
How do SAT solvers work in practice? Decision heuristics.
There will be a set of papers to read over the course.
The format will be lecture and discussion, with a small amount of homework.
We meet at 10.15 on Mondays (room 2103) and Thursdays (room 2101)
List of talks
- 04/09 SAT, general discussions (Fedor)
- 07/09 Solving 3-SAT (Fedor)
- 11/09 Paturi, Pudlak, Saks, and Zane paper (Igor)
- 14/09 No lectures this day
- 18/09 Paturi, Pudlak, Saks, and Zane paper (Igor)
- 22/09New technique for solving sparse equation systems (Havard)
- 25/09 New technique for solving sparse equation systems (Havard)
- 28/09 (Igor)
- Oliver Kullmann, Worst-case Analysis, 3-SAT Decision and Lower Bounds: Approaches for Improved SAT Algorithms.
- Oliver Kullmann, New methods for 3-SAT decision and worst-case analysis.
- Ryan Williams,
A new algorithm for optimal 2-constraint satisfaction and its implications.
- Dantsin, Evgeny; Goerdt, Andreas; Hirsch, Edward A.; Kannan, Ravi; Kleinberg, Jon; Papadimitriou, Christos; Raghavan, Prabhakar; Scho"ning, Uwe
A deterministic $(2-2/(k+1))\sp n$ algorithm for $k$-SAT based on local search.
- Uwe Schoening,
Algorithmics in Exponential Time.
- Ramamohan Paturi, Pavel Pudla'k, Michael E. Saks, Francis Zane,
An improved exponential-time algorithm for k-SAT.
- H. Raddum and I. Semaev,
New technique for solving sparse equation systems.
- Martin Davis and
Hilary Putnam A Computing Procedure for Quantification Theory .
M.Davis, G.Logemann, and D.Loveland
A machine program for theorem-proving .
The first lecture: September 4, at 10.15 in Grupperom 2103, Hoyteknologisenteret