Other years: [Autumn 2002] [Autumn 2000]

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 13th of September
• Registration by TOPI or by attending the first two lectures
• Lectures by Tomi Janhunen, on Thursdays, 14-16, room TB353
• Tutorials by Tommi Syrjänen, on Tuesdays, 15-16, room TB353
• Course material: lecture notes and articles
• In order to pass the course one has to pass
  • three home assignments and
  • an exam.
• Newsgroup: opinnot.tik.logiikka
• Brochure in Finnish
• Course information at TOPI

Examinations

• May 28, 2002, 12-15, T3
• May 28, 2002, final results (June 4, 2002)
• January 8, 2002, final results (Feb 13, 2002)
• December 19, 2001, final results (Feb 6, 2002)

Home Assignments

• Personal directories for distributing the home assignments will appear here.
• Results
• Submission by email (preferably an URL to visit) to Tommi.Syrjanen@hut.fi or
  in print (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.

Software

boole

• Developed by David Long, the source code 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 >).

sat solvers

• Crawford's ntab: [CA96], source code
• relsat by Bayardo and Schrag: [BS97], source code
• Li's satz: [L99], source code
• chaff by Moskewicz et al.: [MMZZM01], binaries
• A collection of benchmarks for testing sat solvers.

satplan

• Developed by Henry Kautz and Bart Selman.
• A short introduction.

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

Schedule

September 13: Lecture 1, no tutorial

Introduction, a refresher on propositional logic (slides in ps and pdf)

September 20: Lecture 2

Binary decision diagrams (slides in ps and pdf; see also [A97])
Tutorial 1 (in ps), solutions (in ps)

September 27: Lecture 3

Home Assignment 1 (slides in ps and pdf)
Davis-Putnam method (slides in ps and pdf; see also [F90])
Tutorial 2 (in ps), solutions (in ps)

October 4: Lecture 4

Implementing the Davis-Putnam method
(slides in ps and pdf; see also [BS97], [CA96], [L99], [MMZZM01])
Tutorial 3 (in ps), no solutions

October 11: Lecture 5

Local search (stochastic) methods (slides in ps and pdf; see also [SKC93])
Tutorial 4 (in ps), solutions (in ps)

October 18: Lecture 6

Planning as satisfiability (slides in ps and pdf; see also [KS92] and [KS96])
Home Assignment 2 (slides in ps and pdf)
Tutorial 5 (in ps), solutions (in ps)

October 25: Lecture 7

Monotonic rule-based reasoning (slides in ps and pdf; see also [DG84])
Tutorial 6 (in ps), solutions (in ps)

November 1: No lecture

No tutorial

November 8: Lecture 8

Non-monotonic rule-based reasoning (slides in ps and pdf; see also [N99])
Tutorial 7 (in ps), solutions (in ps)

November 15: Lecture 9

Planning as rule-based reasoning, remarks on computational complexity (slides in ps and pdf; see also [N99])
Tutorial 8 (in ps), solutions (in ps)

November 22: Lecture 10

Implementation techniques (slides in ps and pdf)
Tutorial 9 (in ps), solutions (in ps)

November 29: No lecture

No tutorial

December 4: Last session (15:15-16:00).

Deadline of the third home assignment, feedback session

Reading List

• [A97] Andersen, H.R.: An Introduction to Binary Decision Diagrams.
• [F90] Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer-Verlag, 1990, pp. 88-93.
• [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. Also published in Annals of Mathematics and Artificial Intelligence 25(3,4):241-273, 1999.
• [SKC93] Selman, B., Kautz, H.A., and Cohen, B.: Local Search Strategies for Satisfiability Testing, 2nd DIMACS Challenge on Cliques, Coloring and Satisfiability, 1993.

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.
• [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.
• [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.
• [L99] Li, C.M.: A Constraint-based Approach to Narrow Search Trees for Satisfiability. Information Processing Letters 71 (1999), 75-80.
• [MMZZM01] Moskewicz, M.M., Madigan, C.F., Zhao, Y., Zhang, L., and Malik, S.: Chaff: Engineering an Efficient SAT Solver, 39th Design Automation Conference, Las Vegas, June 2001.