T-79.7001 Postgraduate Course in Theoretical Computer Science (2–10 cr) P V

Autumn 2005

Recent developments in general search and reasoning techniques developed in the areas of boolean satisfiability (SAT) and constraint satisfaction problems (CSPs) now allow us to solve combinatorial problems with tens of thousand variables and millions constraints. This dramatic increase in feasible problem size has led to a series of new applications in areas like computer-aided verification, planning, scheduling, supply-chain management, ...

One of the driving forces of this interesting continuing development is combining strengths of SAT and CSP and mathematical (linear/integer) programming techniques. During the seminar we investigate recent developments in this area and, in particular, study closely promising work carried out in the areas of (i) generalized SAT solvers, (ii) pseudo-boolean solvers, (iii) satisfiability modulo theories, (iv) combinations of constraint satisfaction and mathematical programming techniques.

The course is arranged in the form of a research seminar where participants give presentations of research papers.

• Teacher: Prof. Ilkka Niemelä, puh. 451 3290, URL: http://www.tcs.hut.fi/~ini/
• Seminars: On Mondays 16-20 hrs, room TB353. The first seminar is on 12.9.2005.
• Brochure in Finnish
• Literature:
  M. Milano (Ed). Constraint and Integer Programming: Toward a Unified Methodology. Kluwer Academic Publishers. 2004. [Link]

  Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL Framework. Ph.D. Dissertation, University of Oregon. [PDF]

  Articles (an incomplete list):

  • M.Bozzano, R.Bruttomesso, A.Cimatti, T.Junttila, P.v.Rossum, S.Schulz, R.Sebastiani. Mathsat: Tight Integration of SAT and Mathematical Decision Procedures. To appear in Journal of Automated Reasoning, Special Issue on SAT, 2005. [ps.gz]
  • Heidi E. Dixon, Matthew L. Ginsberg, Andrew J. Parkes. Generalizing Boolean Satisfiability I: Background and Survey of Existing Work. Journal of Artificial Intelligence Research, Volume 21, pages 193-243. [link]
  • Heidi E. Dixon, Matthew L. Ginsberg, Eugene M. Luks, Andrew J. Parkes. Generalizing Boolean Satisfiability II: Theory. Journal of Artificial Intelligence Research, Volume 22, pages 481-534. [link]
  • Dixon, H.E., Ginsberg, M.L., Hofer, D., Luks, E.M. and Parkes, A.J. Generalizing Boolean Satisfiability III: Implementation, Journal of Artificial Intelligence Research, Volume 23, pages 441-531. [link]
  • Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. DPLL(T): Fast Decision Procedures. 16th International Conference on Computer Aided Verification (CAV), July 2004, Boston (USA). [PDF]
  • M.Bozzano, R.Bruttomesso, A.Cimatti, T.Junttila, S.Ranise, P.v.Rossum, R.Sebastiani. Efficient Satisfiability Modulo Theories via Delayed Theory Combination. Conference on Computer Aided Verification (CAV 2005). Edinburgh, U.K., July 6-10 2005. [ps.gz]
• Course homepage: http://www.tcs.hut.fi/Studies/T-79.7001/
• Related material

  First International Summer School on Constraint Programming, Hotel Villa del Mare Acquafredda di Maratea -- Italy September 11-15, 2005