|
T-79.154 Logic in Computer Science: Special Topics II (2 cr)
Autumn 2002
[General Information]
[Lectures]
[Feedback]
[Examinations]
[Home assignments]
[Software]
[TOPI]
Previous years:
[Autumn 2001]
[Autumn 2000]
[Autumn 1999]
[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 (Davis-Putnam, BDDs,
stochastic methods) and for rule-based reasoning.
- The course starts on the 12th of September
- Registration: using
TOPI
or by attending the first two lectures
- Lectures by D.Sc.(Tech.)
Tomi Janhunen,
Thursday, 14-16, room TB353
- Tutorials by M.Sc.(Tech.)
Tommi Syrjänen,
Tuesday, 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)
- Brochure
(.ps 50kB/
.pdf 64kB)
in Finnish and English
- Office hours: please see the lecturer's home page.
- Email contacts: please use the alias
t79154
at tcs.hut.fi .
- Newsgroup:
opinnot.tik.logiikka
- 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.
Schedule for Autumn 2002
-
September 12:
Lecture 1
(.ps.gz / .pdf)
- Introduction, a refresher on propositional logic
September 17:
Tutorial 1
(.ps.gz / .pdf),
solutions
(.ps.gz / .pdf)
-
September 19: No lectures nor tutorials this week
-
September 26: No lectures nor tutorials this week
-
October 3:
Lecture 2
(.ps.gz / .pdf)
- Binary decision diagrams (please consult [A97])
Home Assignment 1
October 8:
Tutorial 2
(.ps.gz / .pdf),
solutions
(.ps.gz / .pdf)
-
October 10:
Lecture 3
(.ps.gz / .pdf)
- Davis-Putnam method (please consult [F90])
October 15:
Tutorial 3
(.ps.gz / .pdf),
solutions
(.ps.gz / .pdf)
-
October 17:
Lecture 4
(.ps.gz / .pdf)
- Implementing the Davis-Putnam method
October 22:
Tutorial 4
(.ps.gz / .pdf),
solutions
(.ps.gz / .pdf)
-
October 24:
Lecture 5
(.ps.gz / .pdf)
- Local (stochastic) search methods (please consult [SKC93])
October 29:
Tutorial 5
(.ps.gz / .pdf),
solutions
(.ps.gz / .pdf)
-
October 31:
Lecture 6
(.ps.gz / .pdf)
- Planning as satisfiability
Home Assignment 2
November 5:
Tutorial 6
(.ps.gz / .pdf),
solutions
(.ps.gz / .pdf)
-
November 7:
Lecture 7
(.ps.gz / .pdf)
- Monotonic rule-based reasoning
November 12:
Tutorial 7
(.ps.gz / .pdf),
solutions
(.ps.gz / .pdf)
-
November 14:
Lecture 8
(.ps.gz / .pdf)
- Non-monotonic rule-based reasoning (please consult [N99])
November 19:
Tutorial 8
(.ps.gz / .pdf),
solutions
(.ps.gz / .pdf)
-
November 21:
Lecture 9
(.ps.gz / .pdf)
- Planning as rule-based reasoning,
some properties of stable models
Home Assignment 3
November 26:
Tutorial 9
(.ps.gz / .pdf),
solutions
(.ps.gz / .pdf)
-
November 28:
Lecture 10
(.ps.gz / .pdf)
- Implementation techniques
December 2:
Tutorial 10
(.ps.gz / .pdf),
solutions
(.ps.gz / .pdf)
-
December 5:
Last session
- Feedback
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.
- [N99] 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
30-June 1, 1998.
- [SKC93] Selman, B., Kautz, H.A., and Cohen, B.:
Local Search Strategies for Satisfiability Testing,
2nd DIMACS Challenge on Cliques, Coloring and Satisfiability, 1993.
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.
- [DG84] Dowling, W.F. and Gallier, J.H.,
Linear-Time Algorithms for Testing the Satisfiability
of Propositional Horn Formulae,
Journal of Logic Programming 3 (1984) 267-284.
- [KS92] Kautz, H. and Selman B.,
Planning as Satisfiability,
Proceeding of the 10th European Conference
on Artificial Intelligence, 1992, John Wiley and Sons, 359-363.
- [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.
- [L99] Li, C.M.:
A Constraint-based Approach to Narrow Search Trees for Satisfiability.
Information Processing Letters 71 (1999), 75-80.
- [MMZZM01] Moskewicz, M.M., Madigan, C.F., Zhao, Y.,
Zhang, L., and Malik, S.:
Chaff: Engineering an Efficient SAT Solver,
39th Design Automation Conference, Las Vegas, June 2001.
Please contact the lecturer in order to get copies
of articles that are not available in the web.
Back to menu.
Feedback
We would like to hear your opinion on this course.
Please use our feedback form.
Back to menu.
Examinations
- December 11, 2002,
final results
(published on January 17, 2003).
- February 3, 2003,
final results
(published on March 4, 2003).
- September 3, 2003, hall T1, 13-16
- Registrations for the exams via TOPI.
Back to menu.
Home Assignments
- Are distributed through personal home directories.
- 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.
- Results
Schedule
- The first home assignment was launched October 10, 2002.
- Deadline: October 25, 2002.
- The second and third home assignment were launched on November 5, 2002.
- Deadlines: November 27, 2002 (2nd) and December 4, 2002 (3rd).
Back to menu.
Software
boole
- Developed by David Long, the
source code
is also available.
- A short introduction and
a simple example
- A filter called translate
converts "if-then-else programs" to boole's syntax
(the filter assumes variables of the form x < number >).
sat solvers
satplan
- Developed by Henry Kautz and Bart Selman.
- A short introduction.
smodels
- Developed by Patrik Simons and Ilkka Niemelä.
- The source code is available
here.
lparse
- Developed by Tommi Syrjänen.
- The source code is available
here.
NOTE: 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/ .
Back to menu.
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 24 July 2003.
Tomi Janhunen
|