|
T-79.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 (Davis-Putnam, BDDs,
stochastic methods) and for rule-based 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, 14-16, room TB353
- Tutorials: Lic.Sc.(Tech.)
Tommi Syrjänen,
Tuesdays, 15-16, 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 12-14, room TB353): Lecture 3
-
Davis-Putnam method
(.pdf)
October 12:
Tutorial 3
(.pdf),
solutions
(.pdf)
-
October 14: Lecture 4
-
Implementing the Davis-Putnam method
(.pdf)
October 19:
Tutorial 4
(.pdf),
solutions are not provided due to the nature of exercises
-
October 22 (exceptionally, Friday 12-14, 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 rule-based reasoning
(.pdf)
November 9:
Tutorial 7
(.pdf),
solutions
(.pdf)
-
November 11: Lecture 8
-
Non-monotonic rule-based 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.:
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.
- [SNS02]
Extending and Implementing the Stable Model Semantics, AIJ 138(1-2), 181-234, June 2002.
Further Reading
- [BS97]
Bayardo,
R.J. and Schrag, R.C.:
Using CSP Look-Back Techniques to Solve Real-World SAT Instances.
In the Proc. of AAAI-97, 203-208.
- [CA96]
Crawford,
J.M. and Auton, L.D.:
Experimental Results on the Crossover Point in Random 3-SAT.
Artificial Intelligence 81 (1996) 1, 31-57.
- [L99] Li, C.M.:
A Constraint-based Approach to Narrow Search Trees for Satisfiability.
Information Processing Letters 71 (1999), 75-80.
- [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 Computer-Aided 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/T-79.154/bin/ . Some linux binaries can
be found from ~tomppa/T-79.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 DIMACS-format 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
|