
T79.5102 
Special Course in Computational Logic 
(4 cr) P V 
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 (DavisPutnam, BDDs,
stochastic methods) and for rulebased reasoning.
General Information
 Please use the TOPI
system for registration. Late registration is possible
by contacting the lecturer.
 This course replaces two former courses:
T79.154
Logic in Computer Science: Special Topics II
and
T79.230
Foundations of AgentBased Computing.
The course contents is based on T79.154 this term.
 Lectures: Prof. (pro tem), D.Sc.(Tech.)
Tomi Janhunen,
Mondays, 1214, room TB353
 Tutorials: M.Sc.(Tech.)
Emilia Oikarinen,
Tuesdays, 1516, room TB353
 Course material: lecture notes and articles
 Brochure in Finnish
 Tentative schedule for lectures
Back to menu.
Course Material
Lecture Notes
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.:
FirstOrder Logic and Automated Theorem Proving.
SpringerVerlag, 1990, pp. 8893.
 [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(34), 241273,
1999.
Further Reading
Back to menu.
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).
Back to menu.
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
Back to menu.
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
Home assignments are to be launched as follows:
 HA1: September 19, 2005; deadline October 3, 2005.
 HA2: October 17, 2004; deadline November 7, 2005.
 HA3: November 14, 2004; deadline December 5, 2005.
Back to menu.
Software
Precompiled programs have been installed in the machines of
computing centre: please consult the subdirectories of
~tomppa/T79.5102/ .
boole
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 3SAT.
Artificial Intelligence 81 (1996) 1, 3157.

relsat developed by R. Bayardo and M. Schrag
(source code)
Publication:
Bayardo,R.J. and Schrag, R.C.:
Using CSP LookBack Techniques to Solve RealWorld SAT Instances.
AAAI97, 203208.

satz developed by C. Li
(source code)
Publication:
Li, C.M.:
A Constraintbased Approach to Narrow Search Trees for Satisfiability.
Information Processing Letters 71 (1999), 7580.

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 SATsolver
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 DIMACSformat 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.
Back to menu.
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 23 May 2006.
Tomi Janhunen
