TCS /
Studies /
T79.154 /
1999
Tik79.154 Logic in Computer Science: Special Topics II
Autumn 1999
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 (DavisPutnam, BDDs,
stochastic methods) and for rulebased reasoning.
[General Information]
[Examinations]
[Home Assignments]
[Software]
[Program]
[Reading List]
 The course starts on the 9th of September
 Registration by
TOPI
or by attending the first two lectures
 Lectures by
Tomi Janhunen,
on Thursdays, 1416, room TB353
 Tutorials by Tommi Syrjänen,
on Thursdays, 1617, 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, 1619, halls ABCDE
 Newsgroup:
opinnot.tik.logiikka
 Brochure in
Finnish
 Course information at
TOPI
The three home assignments
were introduced on November 11, 18 and 25.
 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.
boole
 Developed by David Long, the
source code
is also available.
 A short introduction and
a simple example
 A filter called translate
converts "ifthenelse 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 ChuMin 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/Tik79.154/bin/.

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)
 DavisPutnam method (see [Fitting, 1990] below)

September 30: Lecture 3,
Tutorial 3
(solutions)
 Rulebased 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)
 Rulebased reasoning II

October 28: Lecture 7,
Tutorial 7
(solutions)
 Implementing rulebased 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
 [Fitting, 1990] Fitting, M.,
FirstOrder Logic and Automated Theorem Proving,
SpringerVerlag, 1990, pp. 8893
 [DG, 1984] Dowling, W.F. and Gallier, J.H.,
LinearTime Algorithms for Testing the Satisfiability
of Propositional Horn Formulae,
Journal of Logic Programming 3 (1984) 267284.
 [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 3SAT
, Artificial Intelligence 81 (1996) 1, 3157.
 [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, 359363.
 [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.
Latest update: May 18, 2000
by Tomi Janhunen