Autumn 2005 (periods I and II)

[General Information] [Course Material] [Feedback] [Examinations] [Home Assignments] [Software] [TOPI]

This is an advanced course on knowledge representation, automated reasoning and decision making. Subjects covered this year are: advanced decision methods for propositional logic (Davis-Putnam, BDDs, stochastic methods) and for rule-based reasoning.

General Information

• Please use the TOPI system for registration. Late registration is possible by contacting the lecturer.
• This course replaces two former courses: T-79.154 Logic in Computer Science: Special Topics II and T-79.230 Foundations of Agent-Based Computing. The course contents is based on T-79.154 this term.
• Lectures: Prof. (pro tem), D.Sc.(Tech.) Tomi Janhunen, Mondays, 12-14, room TB353
• Tutorials: M.Sc.(Tech.) Emilia Oikarinen, Tuesdays, 15-16, room TB353
• Course material: lecture notes and articles
• Brochure in Finnish
• Tentative schedule for lectures

Course Material

Lecture Notes

• Introduction (.pdf)
• A refresher on propositional logic (.pdf)
• Binary decision diagrams (.pdf); see also [A97].
• Home assignments I (.pdf)
• Davis-Putnam method (.pdf); see also [F90].
• Implementing Davis-Putnam method (.pdf)
• Local search methods (.pdf); see also [SKC93]
• Planning as a satisfiability problem (.pdf); see also [KS96]
• Home assignments II (.pdf)
• Monotonic rule-based reasoning (.pdf)
• Nonmonotonic rule-based reasoning (.pdf)
• Planning as a stability problem (.pdf)
• Implementation techniques (.pdf)
• From stability to propositional satisfiability (.pdf)

Excercises from Tutorials

• Tutorial 1 (.pdf), solutions (.pdf)
• Tutorial 2 (.pdf), solutions (.pdf)
• Tutorial 3 (.pdf), solutions (.pdf)
• Tutorial 4 (.pdf), no solutions (a demo)
• Tutorial 5 (.pdf), solutions (.pdf)
• Tutorial 6 (.pdf), solutions (.pdf)
• Tutorial 7 (.pdf), solutions (.pdf)
• Tutorial 8 (.pdf), solutions (.pdf)
• Tutorial 9 (.pdf), solutions (.pdf)
• Tutorial 10 (.pdf), solutions (.pdf)
• Tutorial 11 (.pdf)

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.
• [KS96] Kautz, H. and Selman, B.: Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search. In 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. In 2nd DIMACS Challenge on Cliques, Coloring and Satisfiability, 1993.
• [N99] Niemelä, I.: Logic Programs with Stable Model Semantics as a Constraint Programming Paradigm. In Annals of Mathematics and Artificial Ingelligence, 24(3-4), 241-273, 1999.

Further Reading

• Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving, Cambridge University Press, 2005.

Course Feedback

We welcome feedback which is collected centrally in Finnish; the questionnaire is activated on the 9th of December, 2005.

• To obtain a 0.5 point bonus for the exams arranged in December and March you are supposed to fill in the form by the 2nd of January, 2006 (24:00 hours).

Examinations

• Please use the TOPI system in order to get registered for an exam.
• December 21, 2005, final results (published, January 19, 2006)
• March 7, 2006, final results (published, April 12, 2006)
• May 9, 2006, no examinees showed up

Home Assignments

• Results
• Home assignments are personal and supposed to be done individually.
• We create a dedicated home directory for each student registered for the course.
• You should expect an email (on September 20, 2005) which gives you access rights to your home directory.
• Submission by email (preferably an URL to visit) to Emilia Oikarinen. Please mention your student ID!
• 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.

Schedule

• HA1: September 19, 2005; deadline October 3, 2005.
• HA2: October 17, 2004; deadline November 7, 2005.
• HA3: November 14, 2004; deadline December 5, 2005.

Software

Precompiled programs have been installed in the machines of computing centre: please consult the subdirectories of ~tomppa/T-79.5102/.

boole

• Developed by D. Long.
• The source code is available at Carnegie Mellon University.
• 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)
  Publication: Crawford,J.M. and Auton, L.D.: Experimental Results on the Crossover Point in Random 3-SAT. Artificial Intelligence 81 (1996) 1, 31-57.
• relsat developed by R. Bayardo and M. Schrag (source code)
  Publication: Bayardo,R.J. and Schrag, R.C.: Using CSP Look-Back Techniques to Solve Real-World SAT Instances. AAAI-97, 203-208.
• satz developed by C. Li (source code)
  Publication: Li, C.M.: A Constraint-based Approach to Narrow Search Trees for Satisfiability. Information Processing Letters 71 (1999), 75-80.
• chaff developed by M. Moskewicz et al. (binaries)
  Publication: Moskewicz, M.M., et al.: Chaff: Engineering an Efficient SAT Solver. 39th Design Automation Conference, Las Vegas, June 2001.
• minisat developed by N. Eén and N. Sörensson (source code and binaries)
  Publication: Eén, N. and Sörensson, N.: An Extensible SAT-solver SAT 2003.
• 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 a satisfiability problem

• Clauses can be instantiated using a program called instantiate.
• As an example, check our encoding of the blocks world domain for instantiate; including an example due to Sussman.
• 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 intp 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.