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

[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 tcs.hut.fi.
• Newsgroup: opinnot.tik.logiikka
• Brochure (.ps 40kB/ .pdf 53kB) in Finnish and English
• Course information at TOPI

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

• [A97] Andersen, H.R.: An Introduction to Binary Decision Diagrams.
• [N99] 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.
• [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.
• [SKC93] Selman, B., Kautz, H.A., and Cohen, B.: Local Search Strategies for Satisfiability Testing, 2nd DIMACS Challenge on Cliques, Coloring and Satisfiability, 1993.
• [SNS02] Extending and Implementing the Stable Model Semantics, AIJ 138(1-2), 181-234, June 2002.

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.

Examinations

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

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 Tommi.Syrjanen@hut.fi .
• 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

Schedule

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

Software

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

boole

• 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

• ntab developed by J. M. Crawford (source code)
• relsat developed by R. Bayardo and M. Schrag (source code)
• satz developed by C. Li (source code)
• chaff developed by M. Moskewicz et al. (binaries)
• A collection of benchmarks for testing 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.