TCS - Studies - T-79.5102 Special Course in Computational Logic

T-79.5102
Special Course in Computational Logic (4 cr) P V
Autumn 2007

This course provides an in-depth introduction to answer set programming (ASP) — a constraint programming paradigm that emerged in the 90s. The paradigm is based on a new interpretation of rules: a set of answer sets is associated with each set of rules viewed as constraints. The idea is that a problem at hand is solved by first describing its solutions using rules so that a tight correspondence of answer sets and solutions is obtained. Then, the solution(s) of the problem can be searched for using special-purpose search engines called answer set solvers.

The success of ASP is much due to efficient answer set solvers available today (see e.g. SMODELS, DLV, and CLASP). Moreover, the expressive power of rules strictly exceeds that of propositional clauses, i.e., the input language of SAT solvers, which favors succinct representations knowledge in a number of domains. A wide range of applications of ASP as emerged as a result of solving challenging computational problems using ASP techniques. In this respect, it is worth mentioning application domains such as

product configuration,
solving combinatorial auctions,
verifying contingency plans for the space shuttle,
information and data integration, and
the analysis of security protocols.

The aim of the course is to familiarize students with the art of declarative problem solving, knowledge representation, and reasoning in the context of ASP. The course introduces ASP, its theoretical background, basic methodology, applications, as well as tools. Moreover, practical programming skills are sought for. The course spans over the first two periods and it consists of a lecture and a tutorial every week. The course requirements include an exam and three compulsory home assignments. Each of them will involve declarative problem solving using methods and tools presented during the course.

Course material: lecture notes and articles.
Supplementary reading: Chitta Baral: Knowledge Representation, Reasoning, and Declarative Problem Solving. First edition. Cambridge University Press, 2003.
Lectures: Mondays, 12—14, room TB353; the course starts on the 17th of September, 2007
Tutorials: Tuesdays, 15—16, room TB353
Lecturer: Docent, D.Sc.(Tech.) Tomi Janhunen, email Tomi.Janhunentkk.fi, home page at http://www.tcs.hut.fi/~ttj/
Course assistant: M.Sc.(Tech.) Antti Hyvärinen, email Antti.Hyvarinentkk.fi
Prerequisites: T-79.3001 Logic in computer science: foundations
Home page of the course: http://www.tcs.hut.fi/Studies/T-79.5102/

An Example

An ASP formulation of the sudoku puzzle: The first solution found by SMODELS (in 0.05s):


number(1..9).


value(1,3,2). ... % clues


 border(1;4;7).


1 { value(X,Y,N):number(X;Y):

    X1<=X:X<=X1+2:Y1<=Y:Y<=Y1+2 } 1

:- number(N), border(X1;Y1).


:- 2 { value(X,Y,N):number(N) }, number(X;Y).


:- 2 { value(X,Y,N):number(X) }, number(N;Y).


:- 2 { value(X,Y,N):number(Y) }, number(N;X).

1	9	3
4	6	8
7	5	2

8	6	7
5	3	2
1	4	9

4	2	5
9	1	7
6	8	3

6	2	1
5	3	4
9	8	7

4	7	3
9	1	8
2	5	6

5	9	8
7	6	2
3	4	1

2	1	6
8	7	5
3	4	9

3	9	5
6	2	4
7	8	1

8	7	4
1	3	9
2	5	6

Gordon Royle's 16-clue sudoku with two solutions

T-79.5102 Special Course in Computational Logic (4 cr) P V Autumn 2007

An Example

T-79.5102
Special Course in Computational Logic (4 cr) P V
Autumn 2007