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 2003

[General Information] [Lectures] [Examinations] [Home assignments] [Software] [TOPI]

Other years: autumns [2004] 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 11th 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: M.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 (.ps 40kB/ .pdf 53kB) in Finnish and English
  • 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.

Schedule for Autumn 2003

September 11: Lecture 1
Introduction (.pdf), a refresher (.pdf) on propositional logic
September 16: Tutorial 1 (solutions)
September 18: Lecture 2
Binary decision diagrams (.pdf)
Home Assignment 1 (.pdf)
September 23: Tutorial 2 (solutions)
September 25: no lecture this week
October 2: Lecture 3
Davis-Putnam method (.pdf)
October 7: Tutorial 3 (solutions)
October 9: Lecture canceled!
October 14: Tutorial canceled!
October 16: Lecture 4
Implementing the Davis-Putnam method (.pdf)
October 21: Tutorial 4 (no solutions)
October 23: Lecture 5
Local (stochastic) search methods (.pdf)
October 28: Tutorial 5 (solutions)
October 30: Lecture 6
Planning as satisfiability (.pdf)
Home Assignment 2; see the Blocks World example
November 4: Tutorial 6 (solutions)
November 6: Lecture 7
Monotonic rule-based reasoning (.pdf)
November 11: Tutorial 7 (solutions)
November 13: Lecture 8
Non-monotonic rule-based reasoning (.pdf)
November 18: Tutorial 8 (solutions)
November 20: Lecture 9
Planning as rule-based reasoning, some properties of stable models (.pdf)
Home Assignment 3
November 25: Tutorial 9 (solutions)
November 27: Lecture 10
Implementation techniques (.pdf)
December 2: Tutorial 10 (solutions)
December 4: Lecture 11
From stable models to propositional satisfiablity (.pdf)
This is supplementary material not required in the exam!
No tutorial

Reading List

Further Reading

  • [BS97] Bayardo, 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.
  • [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.
  • [L99] Li, C.M.: A Constraint-based Approach to Narrow Search Trees for Satisfiability. Information Processing Letters 71 (1999), 75-80.
  • [MZZMM01] Moskewicz, M.M., et al.: Chaff: Engineering an Efficient SAT Solver. 39th Design Automation Conference, Las Vegas, June 2001.
  • [ZMMM01] 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.


  • Registrations for the exams via TOPI.
  • December 10, 2003, final results (published on Jan 14, 2004)
  • February 16, 2004, final results (published on Mar 30, 2004)
  • May 10, 2004, final results (published on May 28, 2004)
Back to menu.

Home Assignments

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


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


  • Developed by D. Long (source code)
  • 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 x1, x2, etc).

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. This is a special edition of lparse targeted to instantiation of propositional clauses.
  • 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: 02 December 2004. Tomi Janhunen