T-79.154 Logic in Computer Science: Special Topics II (2 cr)
Other years: autumns
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.
Back to menu.
- The course starts on the 11th of September
- Registration: using
or by attending the first two lectures
- Lectures: docent, D.Sc.(Tech.)
Thursdays, 14-16, room TB353
- Tutorials: M.Sc.(Tech.)
Tuesdays, 15-16, room TB353
- Course material:
lecture notes and articles
- In order to pass the course one has to
- pass the home assignments
- pass the exam (with a grade greater than 0)
- Office hours: please see the lecturer's home page.
- Email contacts: please use the alias
in Finnish and English
- Course information at
- Slides from lectures are provided in an electronic form.
- Exercises and solutions presented at tutorials will be also included.
- Further references are available in the reading list below.
Schedule for Autumn 2003
September 11: Lecture 1
(.pdf) on propositional logic
September 18: Lecture 2
Binary decision diagrams
Home Assignment 1
September 25: no lecture this week
October 2: Lecture 3
October 9: Lecture canceled!
- October 14: Tutorial canceled!
October 16: Lecture 4
the Davis-Putnam method
October 23: Lecture 5
October 30: Lecture 6
Planning as satisfiability
Home Assignment 2;
see the Blocks World example
November 6: Lecture 7
Monotonic rule-based reasoning
November 13: Lecture 8
Non-monotonic rule-based reasoning
November 20: Lecture 9
Planning as rule-based reasoning,
some properties of stable models
Home Assignment 3
November 27: Lecture 10
December 4: Lecture 11
From stable models to propositional satisfiablity
This is supplementary material not required in the exam!
- [A97] Andersen, H.R.:
An Introduction to Binary Decision Diagrams.
- [N99] Niemelä, I.:
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.
- [KS96] Kautz, H. and
Pushing the Envelope: Planning, Propositional Logic,
and Stochastic Search,
Proceedings of the 13th National Conference on Artificial
Intelligence, Portland, OR, 1996.
Selman, B., Kautz, H.A., and Cohen, B.:
Local Search Strategies for Satisfiability Testing,
2nd DIMACS Challenge on Cliques, Coloring and Satisfiability, 1993.
Extending and Implementing the Stable Model Semantics, AIJ 138(1-2), 181-234, June 2002.
R.J. and Schrag, R.C.:
Using CSP Look-Back Techniques to Solve Real-World SAT Instances.
In the Proc. of AAAI-97, 203-208.
J.M. and Auton, L.D.:
Experimental Results on the Crossover Point in Random 3-SAT.
Artificial Intelligence 81 (1996) 1, 31-57.
- [L99] Li, C.M.:
A Constraint-based Approach to Narrow Search Trees for Satisfiability.
Information Processing Letters 71 (1999), 75-80.
M.M., et al.: Chaff: Engineering an Efficient SAT Solver.
39th Design Automation Conference, Las Vegas, June 2001.
Zhang, L. et al.:
: Efficient Conflict Driven Learning in a Boolean Satisfiability
Solver. In the Proc. of International Conference on Computer-Aided Design
(ICCAD 2001), San Jose, CA, November 2001.
Please contact the lecturer in order to get copies
of articles that are not available in the web.
Back to menu.
Back to menu.
- Registrations for the exams via TOPI.
- December 10, 2003,
(published on Jan 14, 2004)
- February 16, 2004,
(published on Mar 30, 2004)
- May 10, 2004,
(published on May 28, 2004)
- Are distributed through
personal home directories.
- You should expect an email (by September 19) which
gives you access rights to your home directory.
- Submission by email (preferably an URL to visit)
- 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.
Back to menu.
- The first home assignment was launched on September 18, 2003.
Deadline: October 9, 2003.
- The second and third home assignments were launched on November 11, 2003.
Deadline: December 4, 2003.
Precompiled programs are available in the machines of
computing centre: please consult the directory
~tssyrjan/T-79.154/bin/. Some linux binaries can
be found from
- Developed by D. Long
- 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
LP instantiators and solvers
lparse developed by T. Syrjänen
smodels developed by P. Simons and I. Niemelä
GnT developed by P. Simons, T. Janhunen, and I. Niemelä
planning as satisfiability
Back to menu.
- Clauses can be instantiated using a program called
is a special edition of
to instantiation of propositional clauses.
- As an example, check our encoding of
the blocks world domain for
- The output of
instantiate is a valid input
GnT that computes minimal models for
the given set of rules/clauses.
- Alternatively, the internal
gnt/smodels format can
be translated into DIMACS-format supported by most SAT solvers
using a translator called
- When using SAT solvers, a filter called
interpret can be
used to printing models in a symbolic (rather than numeric) form.
- See some examples how
the programs are used to solving planning problems.
Latest update: 02 December 2004.