Tik-79.154 Logic in Computer Science: Special Topics II
This is an advanced course on logic and its applications in computer
science and engineering. Subjects covered this year are:
advanced decision methods for propositional logic (Davis-Putnam, BDDs,
stochastic methods) and for rule-based reasoning.
- The course starts on the 9th of September
- Registration by
or by attending the first two lectures
- Lectures by
on Thursdays, 14-16, room TB353
- Tutorials by
on Tuesdays, 16-17, room TB353
- Course material:
lecture notes and articles
- In order to pass the course one has to pass
- three home assignments and
- an exam.
- Brochure in
- Course information at
- Home assignments
are available in the web.
- DEADLINE: November 16, 2000.
- Submission by email (preferably an URL to visit)
to Tommi.Syrjanen@hut.fi or
(a white mailbox outside room TB336).
- Your report should include a short description
of your approach/solution (including the translation involved),
solutions (or counter examples) found and sample
runs (if appropriate).
- The first home assignment involves large boolean
functions (and quite large files).
Please do not send
such big files (or their translations) to us.
- Developed by David Long, the
is also available.
- A short introduction and
a simple example
- A filter called translate
converts "if-then-else programs" to boole's syntax
(the filter assumes variables of the form x< number >).
- Developed by Henry Kautz and Bart Selman, the
is also available.
- A short introduction.
- There are several solvers to be used with satplan:
- ntab (by James Crawford)
- posit (by Jon Freeman)
- relsat (by R. Bayardo Jr. and R. Schrag)
- sato (by Hantao Zhang)
- satz (by Chu-Min Li)
- walksat (by H. Kautz and B. Selman) is distributed with satplan
- Developed by Ilkka Niemelä and Patrik Simons, the
is also available.
- A parser
developed by Tommi Syrjänen
provides support for rules with variables
Precompiled programs are available in the machines of
computing centre: please consult the directory
September 14: Lecture 1, no tutorial
- Introduction, a refresher on propositional logic
September 21: Lecture 2,
- Rule-based Reasoning I (see [DG84])
September 28: No lecture
October 5: Lecture 3,
- Davis-Putnam method (see [F90], [LA97])
October 12: Lecture 4,
- Stochastic methods (see [SKC] and [CA96])
October 19: Lecture 5,
- Binary Decision Diagrams (see [Andersen97] and [Bryant86])
October 26: Lecture 6,
- Rule-based Reasoning II (see [Niemelä99])
November 2: No lecture
November 9: Lecture 7
- Implementation techniques: smodels and
November 16: Lecture 8
- Planning as satisfiability (see [KS92] and [KS96]),
November 23: Lecture 9
- Planning with stable models, remarks on the
complexity of computing stable models
November 30: No lecture
December 7: Guest lecture
- Tommi Junttila: (title to be announced)
Please contact the lecturer in order to get copies
of articles that are not available in the web.
- [F90] Fitting, M.,
First-Order Logic and Automated Theorem Proving,
Springer-Verlag, 1990, pp. 88-93
[DG84] Dowling, W.F. and Gallier, J.H.,
Linear-Time Algorithms for Testing the Satisfiability
of Propositional Horn Formulae,
Journal of Logic Programming 3 (1984) 267-284.
[LA97] Li, C.M. and Anbulagan,
Look-Ahead Versus Look-Back for Satisfiability Problems
, Proceedings of the 3rd International Coference on
Principles and Practice of Constraint Programming, CP97,
Linz, Austria, 1997, pp. 341-355.
- [SKC] Selman, B., Kautz, H. and Cohen B.,
Local Search Strategies for Satisfiability Testing
Dimacs Series in Discrete Mathematics and Theoretical Computer Science.
- [CA96] Crawford, J.M. and Auton, L.D.,
Experimental Results on the Crossover Point in Random 3-SAT
, Artificial Intelligence 81 (1996) 1, 31-57.
- [Andersen97] Andersen, H.R.,
An Introduction to Binary Decision Diagrams.
- [Bryant86] Bryant, R.E.,
Graph-Based Algorithms for Boolean Function Manipulation,
IEEE Transactions of Computers, C-35(8), August, 1986.
- [Niemelä99] Niemelä, I.,
Logic Programs with Stable Model Semantics as
a Constraint Programming Paradigm,
An extended version of the paper presented at the Workshop on
Computational Aspects of Nonmonotonic Reasoning, Trento, Italy, May
30-June 1, 1998. Also published in Annals of Mathematics and
Artificial Intelligence 25(3,4):241-273, 1999.
- [KS92] Kautz, H. and Selman B.,
Planning as Satisfiability,
Proceeding of the 10th European Conference
on Artificial Intelligence, 1992, John Wiley and Sons, 359-363.
- [KS96] Kautz, H. and Selman B., Pushing the Envelope: Planning,
Propositional Logic, and Stochastic Search,
Proceedings of the 13th National Conference on Artificial
Intelligence, Portland, OR, 1996.
Latest update: June 1, 2001
by Tomi Janhunen