Other years: [Autumn 2000] [Autumn 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 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 Thursdays, 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
• The first exam: December 15, 1999, 16-19, halls ABCDE
• Newsgroup: opinnot.tik.logiikka
• Brochure in Finnish
• Course information at TOPI

Examinations

• December 15, 1999, results
• May 22, 2000, results

Home Assignments

• Home assignments are available in the web.
• Please consult the list of accepted assignments.
• Submission by email (preferably an URL to visit) to tssyrjan@saturn.tcs.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 (or will be) available in the machines of computing centre:
please consult the directory ~tssyrjan/Tik-79.154/bin/.

Program

September 9: Lecture 1, no tutorial

Introduction, a refresher on propositional logic

September 16: No lecture, Tutorial 1 (solutions)

Reducing graph problems to propositional decision problems

September 23: Lecture 2, Tutorial 2 (solutions)

Davis-Putnam method (see [Fitting, 1990] below)

September 30: Lecture 3, Tutorial 3 (solutions)

Rule-based reasoning (see [DG,1984] below)

October 7: Lecture 4, Tutorial 4 (solutions)

Local search methods (see [SKC] and [CA, 1996] below)

October 14: Lecture 5, Tutorial 5 (solutions)

Binary decision diagrams (see [Andersen, 1997] below)

October 21: Lecture 6, Tutorial 6 (solutions)

Rule-based reasoning II

October 28: Lecture 7, Tutorial 7 (solutions)

Implementing rule-based reasoning

November 4: Lecture 8a, Lecture 8b, no tutorial

Rules with variables & Planning as satisfiability (see [KS, 1992 and 1996] below)

November 11: Lecture 9, Tutorial 8 (solutions)

Planning with logic programs, complexity issues (see [CA, 1996] below) & HA1

November 18: Introduction to HA2 and HA3

Help for the first home assignment

November 25: No lecture

Help for home assignments, 15:15 - 17:00, by Tommi Syrjänen

December 2: No lecture

Help for home assignments, 15:15 - 17:00, by Tommi Syrjänen

Reading List

• [Fitting, 1990] Fitting, M., First-Order Logic and Automated Theorem Proving, Springer-Verlag, 1990, pp. 88-93
• [DG, 1984] 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.
• [SKC] Selman, B., Kautz, H. and Cohen B., Local Search Strategies for Satisfiability Testing , Dimacs Series in Discrete Mathematics and Theoretical Computer Science.
• [CA, 1996] Crawford, J.M. and Auton, L.D., Experimental Results on the Crossover Point in Random 3-SAT , Artificial Intelligence 81 (1996) 1, 31-57.
• [Andersen, 1997] Andersen, H.R., An Introduction to Binary Decision Diagrams.
• [KS, 1992] Kautz, H. and Selman B., Planning as Satisfiability, Proceeding of the 10th European Conference on Artificial Intelligence, 1992, John Wiley and Sons, 359-363.
• [KS, 1996] 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.