T-79.7001 Postgraduate Course in Theoretical Computer Science (2–10 cr)
[The course T-79.7001 replaces the course
T-79.300 Postgraduate Course in Theoretical Computer Science
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
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.
Prof. Ilkka Niemelš, puh. 451 3290,
- Seminars: On Mondays 16-20 hrs, room TB353.
The first seminar is on 12.9.2005.
- Brochure in Finnish
M. Milano (Ed). Constraint and Integer Programming: Toward a Unified
Methodology. Kluwer Academic Publishers. 2004.
Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a
DPLL Framework. Ph.D. Dissertation, University of Oregon.
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,
- 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
- 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.
- 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.
- 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).
- M.Bozzano, R.Bruttomesso, A.Cimatti, T.Junttila, S.Ranise,
Efficient Satisfiability Modulo Theories via Delayed Theory Combination.
Conference on Computer Aided Verification (CAV 2005).
Edinburgh, U.K., July 6-10 2005.
- Course homepage: http://www.tcs.hut.fi/Studies/T-79.7001/
- Related material
International Summer School on Constraint Programming,
Hotel Villa del Mare
Acquafredda di Maratea -- Italy
September 11-15, 2005
Latest update: 03 January 2006.