
T79.154 Logic in Computer Science: Special Topics II (2 cr)
Autumn 2004
[General Information]
[Lectures and Tutorials]
[Feedback]
[Examinations]
[Home assignments]
[Software]
[TOPI]
Previous years: autumns
[2003]
[2002]
[2001]
[2000]
[1999]
[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.
 The course starts on the 16th of September
 Registration: using
TOPI
or by attending the first two lectures
 Lectures: Docent, D.Sc.(Tech.)
Tomi Janhunen,
Thursdays, 1416, room TB353
 Tutorials: Lic.Sc.(Tech.)
Tommi Syrjänen,
Tuesdays, 1516, 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)
 Office hours: please see the lecturer's home page.
 Email contacts: please use the alias
t79154
at tcs.hut.fi .
 Newsgroup:
opinnot.tik.logiikka
 Brochure
(.pdf)
in Finnish
 Course information at
TOPI
Back to menu.
Lecture Notes
 Slides from lectures are provided in an electronic form.
 Exercises and solutions presented at tutorials will be also included.
 Further references are available in the reading list below.
Tentative Schedule for Autumn 2004

September 16: Lecture 1

Introduction
(.pdf),
a refresher on propositional logic
(.pdf)
September 21:
Tutorial 1
(.pdf),
solutions
(.pdf)

September 23: Lecture 2

Binary decision diagrams
(.pdf)
Home assignment 1
(.pdf)
September 28:
no tutorial this week

September 30: no lecture this week
 October 5:
Tutorial 2
(.pdf),
solutions
(.pdf)

October 8 (exceptionally Friday 1214, room TB353): Lecture 3

DavisPutnam method
(.pdf)
October 12:
Tutorial 3
(.pdf),
solutions
(.pdf)

October 14: Lecture 4

Implementing the DavisPutnam method
(.pdf)
October 19:
Tutorial 4
(.pdf),
solutions are not provided due to the nature of exercises

October 22 (exceptionally, Friday 1214, room TB353): Lecture 5

Local (stochastic) search methods
(.pdf)
October 27:
Tutorial 5
(.pdf),
solutions
(.pdf)

October 28: Lecture 6

Planning as a satisfiability problem
(.pdf)
Home Assignment 2
(.pdf)
and the Blocks World example
November 2:
Tutorial 6
(.pdf),
solutions
(.pdf)

November 4: Lecture 7

Monotonic rulebased reasoning
(.pdf)
November 9:
Tutorial 7
(.pdf),
solutions
(.pdf)

November 11: Lecture 8

Nonmonotonic rulebased reasoning
(.pdf)
November 16:
Tutorial 8
(.pdf),
solutions
(.pdf)

November 18: Lecture 9

Planning as a stability problem, some properties of stable models
(.pdf)
Home Assignment 3
November 23:
Tutorial 9
(.pdf),
solutions
(.pdf)

November 25: Lecture 10

Implementation techniques
(.pdf)
November 30:
Tutorial 10
(.pdf)

December 2: Lecture 11

From
stability to propositional satisfiablity:
representing normal programs with clauses
(.pdf)
December 7:
Tutorial 11 (help for home assignments if needed)
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.
 [SNS02]
Extending and Implementing the Stable Model Semantics, AIJ 138(12), 181234, June 2002.
Further Reading
 [BS97]
Bayardo,
R.J. and Schrag, R.C.:
Using CSP LookBack Techniques to Solve RealWorld SAT Instances.
In the Proc. of AAAI97, 203208.
 [CA96]
Crawford,
J.M. and Auton, L.D.:
Experimental Results on the Crossover Point in Random 3SAT.
Artificial Intelligence 81 (1996) 1, 3157.
 [L99] Li, C.M.:
A Constraintbased Approach to Narrow Search Trees for Satisfiability.
Information Processing Letters 71 (1999), 7580.
 [MZZMM01]
Moskewicz,
M.M., et al.: Chaff: Engineering an Efficient SAT Solver.
39th Design Automation Conference, Las Vegas, June 2001.
 [ZMMM01]
Zhang, L. et al.
: Efficient Conflict Driven Learning in a Boolean Satisfiability
Solver. In the Proc. of International Conference on ComputerAided Design
(ICCAD 2001), San Jose, CA, November 2001.
Please contact the lecturer in order to get copies
of articles that are not available in the web.
Back to menu.
Course Feedback
We welcome feedback which is collected centrally in
Finnish,
Swedish, or
English.
Back to menu.
Examinations
 Please use the TOPI system in order to get registered for an exam.
 December 13, 2004,
final results
(published Jan 19, 2005)
 February 14, 2005,
final results
(published Mar 23, 2005)
 May 10, 2005,
final results
(published Jun 7, 2005)
Back to menu.
Home Assignments
 Are distributed through
personal home directories.
 You should expect an email (by September 24, 2004) which
gives you access rights to your home directory.
 Submission by email (preferably an URL to visit)
to
Tommi.Syrjanen@hut.fi . 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.
 Results
Schedule
Home assignments were launched follows:
 Home Assignment 1: September 24, 2004; deadline October 8, 2004.
 Home Assignment 2: October 28, 2004; deadline November 11, 2004.
 Home Assignment 3: October 28, 2004; deadline November 25, 2004.
Back to menu.
Software
Precompiled programs are available in the machines of
computing centre: please consult the directory
~tssyrjan/T79.154/bin/ . Some linux binaries can
be found from ~tomppa/T79.154/bin/ .
boole
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 satisfiability
 Clauses can be instantiated using a program called
instantiate.
 As an example, check our encoding of
the blocks world domain for
instantiate .
 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
interpret 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: 26 September 2005.
Tomi Janhunen
