TCS / Studies / T-79.7001 Postgraduate Course in Theoretical Computer Science
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

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

Autumn 2005


[The course T-79.7001 replaces the course T-79.300 Postgraduate Course in Theoretical Computer Science .]


Previous years: [Spring 2005] [Autumn 2004] [Spring 2004] [Autumn 2003] [Spring 2003] [Autumn 2002] [Spring 2002] [Autumn 2001] [Spring 2001]


The topic for Autumn 2005: Combining SAT, CSP and IP

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


[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 03 January 2006. Ilkka Niemelš