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

Autumn 2002

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

Previous years: [Autumn 2001] [Autumn 2000] [Autumn 1999] [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 12th of September
• Registration: using TOPI or by attending the first two lectures
• Lectures by D.Sc.(Tech.) Tomi Janhunen, Thursday, 14-16, room TB353
• Tutorials by M.Sc.(Tech.) Tommi Syrjänen, Tuesday, 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)
• Brochure (.ps 50kB/ .pdf 64kB) in Finnish and English
• Office hours: please see the lecturer's home page.
• Email contacts: please use the alias t79154 at tcs.hut.fi.
• Newsgroup: opinnot.tik.logiikka
• 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.

Schedule for Autumn 2002

September 12: Lecture 1 (.ps.gz / .pdf)

Introduction, a refresher on propositional logic
September 17: Tutorial 1 (.ps.gz / .pdf), solutions (.ps.gz / .pdf)

September 19: No lectures nor tutorials this week

September 26: No lectures nor tutorials this week

October 3: Lecture 2 (.ps.gz / .pdf)

Binary decision diagrams (please consult [A97])
Home Assignment 1
October 8: Tutorial 2 (.ps.gz / .pdf), solutions (.ps.gz / .pdf)

October 10: Lecture 3 (.ps.gz / .pdf)

Davis-Putnam method (please consult [F90])
October 15: Tutorial 3 (.ps.gz / .pdf), solutions (.ps.gz / .pdf)

October 17: Lecture 4 (.ps.gz / .pdf)

Implementing the Davis-Putnam method
October 22: Tutorial 4 (.ps.gz / .pdf), solutions (.ps.gz / .pdf)

October 24: Lecture 5 (.ps.gz / .pdf)

Local (stochastic) search methods (please consult [SKC93])
October 29: Tutorial 5 (.ps.gz / .pdf), solutions (.ps.gz / .pdf)

October 31: Lecture 6 (.ps.gz / .pdf)

Planning as satisfiability
Home Assignment 2
November 5: Tutorial 6 (.ps.gz / .pdf), solutions (.ps.gz / .pdf)

November 7: Lecture 7 (.ps.gz / .pdf)

Monotonic rule-based reasoning
November 12: Tutorial 7 (.ps.gz / .pdf), solutions (.ps.gz / .pdf)

November 14: Lecture 8 (.ps.gz / .pdf)

Non-monotonic rule-based reasoning (please consult [N99])
November 19: Tutorial 8 (.ps.gz / .pdf), solutions (.ps.gz / .pdf)

November 21: Lecture 9 (.ps.gz / .pdf)

Planning as rule-based reasoning, some properties of stable models
Home Assignment 3
November 26: Tutorial 9 (.ps.gz / .pdf), solutions (.ps.gz / .pdf)

November 28: Lecture 10 (.ps.gz / .pdf)

Implementation techniques
December 2: Tutorial 10 (.ps.gz / .pdf), solutions (.ps.gz / .pdf)

December 5: Last session

Feedback

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.

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

Please contact the lecturer in order to get copies of articles that are not available in the web.

Feedback

We would like to hear your opinion on this course. Please use our feedback form.

Examinations

• December 11, 2002, final results (published on January 17, 2003).
• February 3, 2003, final results (published on March 4, 2003).
• September 3, 2003, hall T1, 13-16
• Registrations for the exams via TOPI.

Home Assignments

• Are distributed through personal home directories.
• 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.
• Results

Schedule

• The first home assignment was launched October 10, 2002.
• Deadline: October 25, 2002.
• The second and third home assignment were launched on November 5, 2002.
• Deadlines: November 27, 2002 (2nd) and December 4, 2002 (3rd).

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.

smodels

• Developed by Patrik Simons and Ilkka Niemelä.
• The source code is available here.

lparse

• Developed by Tommi Syrjänen.
• The source code is available here.

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