Other years: [Autumn 2001] [Autumn 1999]

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 9th 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, 16-17, 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

• December 11, 2000, results
• May 16, 2001, results

Home Assignments

• Home assignments are available in the web.
• Results
• DEADLINE: November 16, 2000.
• 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 >).

satplan

• Developed by Henry Kautz and Bart Selman, the source code is also available.
• A short introduction.
• There are several solvers to be used with satplan:
  • ntab (by James Crawford)
  • posit (by Jon Freeman)
  • relsat (by R. Bayardo Jr. and R. Schrag)
  • sato (by Hantao Zhang)
  • satz (by Chu-Min Li)
  • walksat (by H. Kautz and B. Selman) is distributed with satplan

smodels

• Developed by Ilkka Niemelä and Patrik Simons, the source code is also available.
• A parser lparse developed by Tommi Syrjänen provides support for rules with variables

Precompiled programs are available in the machines of computing centre: please consult the directory ~tssyrjan/Tik-79.154/bin/.

Program

September 14: Lecture 1, no tutorial

Introduction, a refresher on propositional logic

September 21: Lecture 2, Tutorial 1 (solutions)

Rule-based Reasoning I (see [DG84])

September 28: No lecture

October 5: Lecture 3, Tutorial 2 (solutions)

Davis-Putnam method (see [F90], [LA97])

October 12: Lecture 4, Tutorial 3 (solutions)

Stochastic methods (see [SKC] and [CA96])

October 19: Lecture 5, Tutorial 4 (solutions)

Binary Decision Diagrams (see [Andersen97] and [Bryant86])

October 26: Lecture 6, Tutorial 5 (solutions)

Rule-based Reasoning II (see [Niemelä99])

November 2: No lecture

November 9: Lecture 7

Implementation techniques: smodels and lparse

November 16: Lecture 8

Planning as satisfiability (see [KS92] and [KS96]), satplan

November 23: Lecture 9

Planning with stable models, remarks on the complexity of computing stable models

November 30: No lecture

December 7: Guest lecture

Tommi Junttila: (title to be announced)

Reading List

• [F90] Fitting, M., First-Order Logic and Automated Theorem Proving, Springer-Verlag, 1990, pp. 88-93
• [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.
• [LA97] Li, C.M. and Anbulagan, Look-Ahead Versus Look-Back for Satisfiability Problems , Proceedings of the 3rd International Coference on Principles and Practice of Constraint Programming, CP97, Linz, Austria, 1997, pp. 341-355.
• [SKC] Selman, B., Kautz, H. and Cohen B., Local Search Strategies for Satisfiability Testing , Dimacs Series in Discrete Mathematics and Theoretical Computer Science.
• [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.
• [Andersen97] Andersen, H.R., An Introduction to Binary Decision Diagrams.
• [Bryant86] Bryant, R.E., Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions of Computers, C-35(8), August, 1986.
• [Niemelä99] 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.
• [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.