
Course Description:
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( kSAT) problem in the Theory of
Algorithms.)
 Main theoretic ideas behind SAT solvers

Describing symmetric ciphers with kSAT instances,
cryptanalytic algebraic attacks via solving SAT problems.

kSAT and graph theoretic problems. 2SAT and MAXCUT.
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 3SAT (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)
 ...
Papers :
 Oliver Kullmann, Worstcase Analysis, 3SAT Decision and Lower Bounds: Approaches for Improved SAT Algorithms.
 Oliver Kullmann, New methods for 3SAT decision and worstcase analysis.
 Ryan Williams,
A new algorithm for optimal 2constraint satisfaction and its implications.
 Dantsin, Evgeny; Goerdt, Andreas; Hirsch, Edward A.; Kannan, Ravi; Kleinberg, Jon; Papadimitriou, Christos; Raghavan, Prabhakar; Scho"ning, Uwe
A deterministic $(22/(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 exponentialtime algorithm for kSAT.
 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 theoremproving .
The first lecture: September 4, at 10.15 in Grupperom 2103, Hoyteknologisenteret
