TCS /
Studies /
T79.154 /
2000
Tik79.154 Logic in Computer Science: Special Topics II
Autumn 2000
Other years:
[Autumn 2001]
[Autumn 1999]
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 Tuesdays, 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.
 Newsgroup:
opinnot.tik.logiikka
 Brochure in
Finnish
 Course information at
TOPI
 Home assignments
are available in the web.
 Results
 DEADLINE: November 16, 2000.
 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.
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 available in the machines of
computing centre: please consult the directory
~tssyrjan/Tik79.154/bin/.

September 14: Lecture 1, no tutorial
 Introduction, a refresher on propositional logic

September 21: Lecture 2,
Tutorial 1
(solutions)
 Rulebased Reasoning I (see [DG84])

September 28: No lecture


October 5: Lecture 3,
Tutorial 2
(solutions)
 DavisPutnam method (see [F90], [LA97])

October 12: Lecture 4,
Tutorial 3
(solutions)
 Stochastic methods (see [SKC] and [CA96])

October 19: Lecture 5,
Tutorial 4
(solutions)
 Binary Decision Diagrams (see [Andersen97] and [Bryant86])

October 26: Lecture 6,
Tutorial 5
(solutions)
 Rulebased Reasoning II (see [Niemelä99])

November 2: No lecture


November 9: Lecture 7
 Implementation techniques: smodels and
lparse

November 16: Lecture 8
 Planning as satisfiability (see [KS92] and [KS96]),
satplan

November 23: Lecture 9
 Planning with stable models, remarks on the
complexity of computing stable models

November 30: No lecture


December 7: Guest lecture
 Tommi Junttila: (title to be announced)
 [F90] Fitting, M.,
FirstOrder Logic and Automated Theorem Proving,
SpringerVerlag, 1990, pp. 8893

[DG84] Dowling, W.F. and Gallier, J.H.,
LinearTime Algorithms for Testing the Satisfiability
of Propositional Horn Formulae,
Journal of Logic Programming 3 (1984) 267284.

[LA97] Li, C.M. and Anbulagan,
LookAhead Versus LookBack for Satisfiability Problems
, Proceedings of the 3rd International Coference on
Principles and Practice of Constraint Programming, CP97,
Linz, Austria, 1997, pp. 341355.
 [SKC] Selman, B., Kautz, H. and Cohen B.,
Local Search Strategies for Satisfiability Testing
,
Dimacs Series in Discrete Mathematics and Theoretical Computer Science.
 [CA96] Crawford, J.M. and Auton, L.D.,
Experimental Results on the Crossover Point in Random 3SAT
, Artificial Intelligence 81 (1996) 1, 3157.
 [Andersen97] Andersen, H.R.,
An Introduction to Binary Decision Diagrams.
 [Bryant86] Bryant, R.E.,
GraphBased Algorithms for Boolean Function Manipulation,
IEEE Transactions of Computers, C35(8), August, 1986.
 [Niemelä99] 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
30June 1, 1998. Also published in Annals of Mathematics and
Artificial Intelligence 25(3,4):241273, 1999.
 [KS92] Kautz, H. and Selman B.,
Planning as Satisfiability,
Proceeding of the 10th European Conference
on Artificial Intelligence, 1992, John Wiley and Sons, 359363.
 [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.
Please contact the lecturer in order to get copies
of articles that are not available in the web.
Latest update: June 1, 2001
by Tomi Janhunen