INF339 - Utvalgte emner i algoritmer og kompleksitet (Advanced Topics in Algorithms and Complexity)

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( k-SAT) problem in the Theory of Algorithms.)
• 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)
• ...

Papers :

• 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

Siden vedlikeholdes av Fedor V. Fomin