TCS / Studies / T-79.154 Logic in Computer Science: Special Topics II
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

T-79.154 Logic in Computer Science: Special Topics II (2 cr)

Autumn 2004

[General Information] [Lectures and Tutorials] [Feedback] [Examinations] [Home assignments] [Software] [TOPI]

Previous years: autumns [2003] [2002] [2001] [2000] [1999] [1997]

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.

General Information

  • The course starts on the 16th of September
  • Registration: using TOPI or by attending the first two lectures
  • Lectures: Docent, D.Sc.(Tech.) Tomi Janhunen, Thursdays, 14-16, room TB353
  • Tutorials: Lic.Sc.(Tech.) Tommi Syrjänen, 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 t79154 at
  • Newsgroup: opinnot.tik.logiikka
  • Brochure (.pdf) in Finnish
  • Course information at TOPI
Back to menu.

Lecture Notes

  • 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.

Tentative Schedule for Autumn 2004

September 16: Lecture 1
Introduction (.pdf), a refresher on propositional logic (.pdf)
September 21: Tutorial 1 (.pdf), solutions (.pdf)
September 23: Lecture 2
Binary decision diagrams (.pdf)
Home assignment 1 (.pdf)
September 28: no tutorial this week
September 30: no lecture this week
October 5: Tutorial 2 (.pdf), solutions (.pdf)
October 8 (exceptionally Friday 12-14, room TB353): Lecture 3
Davis-Putnam method (.pdf)
October 12: Tutorial 3 (.pdf), solutions (.pdf)
October 14: Lecture 4
Implementing the Davis-Putnam method (.pdf)
October 19: Tutorial 4 (.pdf), solutions are not provided due to the nature of exercises
October 22 (exceptionally, Friday 12-14, room TB353): Lecture 5
Local (stochastic) search methods (.pdf)
October 27: Tutorial 5 (.pdf), solutions (.pdf)
October 28: Lecture 6
Planning as a satisfiability problem (.pdf)
Home Assignment 2 (.pdf) and the Blocks World example
November 2: Tutorial 6 (.pdf), solutions (.pdf)
November 4: Lecture 7
Monotonic rule-based reasoning (.pdf)
November 9: Tutorial 7 (.pdf), solutions (.pdf)
November 11: Lecture 8
Non-monotonic rule-based reasoning (.pdf)
November 16: Tutorial 8 (.pdf), solutions (.pdf)
November 18: Lecture 9
Planning as a stability problem, some properties of stable models (.pdf)
Home Assignment 3
November 23: Tutorial 9 (.pdf), solutions (.pdf)
November 25: Lecture 10
Implementation techniques (.pdf)
November 30: Tutorial 10 (.pdf)
December 2: Lecture 11
From stability to propositional satisfiablity: representing normal programs with clauses (.pdf)
December 7: Tutorial 11 (help for home assignments if needed)

Reading List

Further Reading

Please contact the lecturer in order to get copies of articles that are not available in the web.

Back to menu.

Course Feedback

We welcome feedback which is collected centrally in Finnish, Swedish, or English.

Back to menu.


  • Please use the TOPI system in order to get registered for an exam.
  • December 13, 2004, final results (published Jan 19, 2005)
  • February 14, 2005, final results (published Mar 23, 2005)
  • May 10, 2005, final results (published Jun 7, 2005)
Back to menu.

Home Assignments

  • Are distributed through personal home directories.
  • You should expect an email (by September 24, 2004) which gives you access rights to your home directory.
  • Submission by email (preferably an URL to visit) to . Please mention your student ID!
  • 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.
  • Results


Home assignments were launched follows:
  • Home Assignment 1: September 24, 2004; deadline October 8, 2004.
  • Home Assignment 2: October 28, 2004; deadline November 11, 2004.
  • Home Assignment 3: October 28, 2004; deadline November 25, 2004.
Back to menu.


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 ~tomppa/T-79.154/bin/.


SAT solvers

LP instantiators and solvers

  • lparse developed by T. Syrjänen (source code)
  • smodels developed by P. Simons and I. Niemelä (source code)
  • GnT developed by P. Simons, T. Janhunen, and I. Niemelä (source code)

Planning as satisfiability

  • Clauses can be instantiated using a program called instantiate.
  • As an example, check our encoding of the blocks world domain for instantiate.
  • The output of instantiate is a valid input for 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 dimacs.
  • 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.
Back to menu.
[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 26 September 2005. Tomi Janhunen

Valid HTML 4.0!