A research project funded by Academy of
Finland (project number 43963)
Aug 1, 1998  Dec 31, 2001
Project leader: Dr. Ilkka
Niemelä
Research Personnel: Patrik Simons, Tommi Syrjänen, Tomi Janhunen, Keijo
Heljanko, Tommi Junttila, Maarit Hietalahti, Antti Huima, Toni Jussila, Misa
Keinänen, Heikki Tauriainen, Harriet Beaver, Matti Järvisalo, Tuomo Pyhälä
Visitors: Prof. JiaHuai You, University of Alberta, Canada, JulSep,
1999
Summary: The goal of the research is to develop a novel constraint programming
paradigm based on default rules and study its applications. During the
project the approach that we are studying based on logic program type
rules and the stable model semantics has had an international
breakthrough. An indication of this is, e.g., a special event on the
subject, ``AAAI Spring 2001 Symposium on Answer Set Programming'' that
was organized in March 2001 in Stanford.
The results obtained in the project have contributed significantly to the
breakthrough. We have shown that rules offer a novel interesting basis
for constraint programming [3]. We have extended the
rule formalism on which the paradigm is based by features that are often
needed in applications. Of these the most essential are priorities and
weights, the possibility to include constraints on weights in the rules
and search for optimal solutions specified by
weights [4,6,22,30].
The computability, complexity and expressivity issues of rulebased
reasoning have been studied extensively
[1,2,5,13,14,15,16,17].
Our implementation of rulebased
reasoning [4,21,23,31,33], the Smodels
system, has become a key reference system in the area with a leading
edge performance.
The Smodels system is used in dozens of research groups all
over the world and it has already been employed in a
number of different applications.
A substantial part of the research in this project has focused on
applications in several promising areas:
product configuration [25,26,27,44]
and, in particular, software
configuration [28,29,46,48],
symbolic model checking [7,8,9,10,11,34,40],
dynamic constraint satisfaction [20,24],
cryptanalysis [12],
implementation techniques for disjunctive logic programs [18],
Bayes networks [32], and
Boolean circuit satisfiability checking [19].
The constraint programming paradigm developed in the project seems to
offer promising applications and interesting projects are already in
progress. For example, in the WeCoTin project on Web configuration technology
in the product data management group led by Prof. Reijo Sulonen at
Helsinki University of Technology Smodels is employed as a basis for
the configuration tool.
Another example is a project of Texas Tech University and United Space
Alliance on developing a decision support system
for the ground controllers of space shuttles which is based on the
rulebased approach studied in our project.
Our own future application work is focusing on symbolic model checking
and software configuration.
Keywords: Default reasoning, constraint programming, product configuration,
symbolic model checking
 1

S. Brass, J. Dix, I. Niemelä, and T.C. Przymusinski.
On the equivalence of the static and disjunctive wellfounded
semantics and its computation.
Theoretical Computer Science, 258(12):523553, May 2001.
 2

Tomi Janhunen.
On the intertranslatability of nonmonotonic logics.
Annals of Mathematics in Artificial Intelligence,
27(14):79128, 1999.
 3

I. Niemelä.
Logic programs with stable model semantics as a constraint
programming paradigm.
Annals of Mathematics and Artificial Intelligence,
25(3,4):241273, 1999.
 4

P. Simons, I. Niemelä, and T. Soininen.
Extending and implementing the stable model semantics.
Artificial Intelligence, 138(12):181234, 2002.
 5

J. Dix, U. Furbach, and I. Niemelä.
Nonmonotonic reasoning: Towards efficient calculi and
implementations.
In Andrei Voronkov and Alan Robinson, editors, Handbook of
Automated Reasoning, Volume II, chapter 19, pages 12411354. Elsevier
Science, Amsterdam, 2001.
 6

I. Niemelä and P. Simons.
Extending the Smodels system with cardinality and weight
constraints.
In Jack Minker, editor, LogicBased Artificial Intelligence,
chapter 21, pages 491521. Kluwer Academic Publishers, 2000.
 7

J. Esparza and K. Heljanko.
Implementing LTL model checking with net unfoldings.
In Proceedings of the 8th International SPIN Workshop on Model
Checking of Software (SPIN'2001), pages 3756, Toronto, Canada, May 2001.
LNCS 2057.
 8

K. Heljanko.
Bounded reachability checking with process semantics.
In Proceedings of the 12th International Conference on
Concurrency Theory (CONCUR'2001), pages 218232, August 2001.
LNCS 2154.
 9

K. Heljanko, V. Khomenko, and M. Koutny.
Parallelisation of the Petri net unfolding algorithm.
In Proceedings of 8th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS'2002), pages
371385, Grenoble, France, April 2002.
LNCS 2280.
 10

K. Heljanko and I. Niemelä.
Answer set programming and bounded model checking.
In Proceedings of the AAAI Spring 2001 Symposium on Answer Set
Programming: Towards Efficient and Scalable Knowledge Representation and
Reasoning, pages 9096, Stanford, USA, March 2001. AAAI Press.
 11

K. Heljanko and I. Niemelä.
Bounded LTL model checking with stable models.
In Proceedings of the 6th International Conference on Logic
Programming and Nonmonotonic Reasoning, pages 200212, Vienna, Austria,
September 2001. SpringerVerlag.
 12

M. Hietalahti, F. Massacci, and I. Niemelä.
DES: a challenge problem for nonmonotonic reasoning systems.
In Proceedings of the 8th International Workshop on
NonMonotonic Reasoning (cs.AI/0003073), Breckenridge, Colorado, USA, April
2000.
cs.AI/0003039.
 13

Tomi Janhunen.
On the intertranslatability of autoepistemic, default and priority
logics, and parallel circumscription.
In J. Dix, L. Fariñas del Cerro, and U. Furbach, editors, Proceedings of the 6th European Workshop on Logics in Artificial
Intelligence, JELIA'98, pages 216232, Dagstuhl, Germany, October 1998.
SpringerVerlag.
LNAI 1489.
 14

Tomi Janhunen.
Classifying seminormal default logic on the basis of its expressive
power.
In M. Gelfond, N. Leone, and G. Pfeifer, editors, Proceedings of
the 5th International Conference on Logic Programming and NonMonotonic
Reasoning, LPNMR'99, pages 1933, El Paso, Texas, December 1999.
SpringerVerlag.
LNAI 1730.
 15

Tomi Janhunen.
Comparing the expressive powers of some syntactically restricted
classes of logic programs.
In J. Lloyd et al., editors, Computational Logic, First
International Conference, pages 852866, London, UK, July 2000.
SpringerVerlag.
LNAI 1861.
 16

Tomi Janhunen.
Capturing stationary and regular extensions with Reiter's
extensions.
In OjedaAciego M. et al., editors, Logics in Artificial
Intelligence, European Workshop, JELIA 2000, pages 102117, Málaga,
Spain, September/October 2000. SpringerVerlag.
LNAI 1919.
 17

Tomi Janhunen.
On the effect of default negation on the expressiveness of
disjunctive rules.
In T. Eiter, W. Faber, and M. Truszczynski, editors, Logic
Programming and Nonmonotonic Reasoning, Proceedings of the 6th International
Conference, pages 93106, Vienna, Austria, September 2001.
 18

T. Janhunen, I. Niemelä, P. Simons, and J. You.
Unfolding partiality and disjunctions in stable model semantics.
In A.G. Cohn, F. Guinchiglia, and B. Selman, editors, Proceedings of the Seventh International Conference on Principles of
Knowledge Representation and Reasoning, pages 411419, Breckenridge,
Colorado, USA, April 2000. Morgan Kaufmann Publishers.
 19

T. Junttila and I. Niemelä.
Towards an efficient tableau method for boolean circuit
satisfiability checking.
In Proceedings of the First International Conference on
Computational Logic, Automated Deduction: Putting Theory into Practice,
pages 553567, London, U.K., July 2000. SpringerVerlag.
 20

I. Niemelä.
On the complexity of dynamic constraint satisfaction.
In Proceedings of the FLoC Workshop on ComplexityTheoretic and
RecursionTheoretic Methods in Databases, Artificial Intelligence and Finite
Model Theory, pages 3847, Trento, Italy, July 1999.
 21

I. Niemelä, P. Simons, and T. Syrjänen.
Smodels: a system for answer set programming.
In Proceedings of the 8th International Workshop on
NonMonotonic Reasoning (cs.AI/0003073), Breckenridge, Colorado, USA, April
2000.
cs.AI/0003033.
 22

I. Niemelä, P. Simons, and T. Soininen.
Stable model semantics of weight constraint rules.
In Proceedings of the 5th International Conference on Logic
Programming and Nonmonotonic Reasoning, pages 317331, El Paso, Texas, USA,
December 1999. SpringerVerlag.
 23

P. Simons.
Extending the stable model semantics with more expressive rules.
In Proceedings of the 5th International Conference on Logic
Programming and Nonmonotonic Reasoning, pages 305316, El Paso, Texas, USA,
December 1999. SpringerVerlag.
 24

T. Soininen, E. Gelle, and I. Niemelä.
A fixpoint definition of dynamic constraint satisfaction.
In Joxan Jaffar, editor, Proceedings of the Fifth International
Conference on Principles and Practice of Constraint Programming, pages
419433, Alexandria, Virginia, USA, October 1999. SpringerVerlag.
 25

T. Soininen and I. Niemelä.
Developing a declarative rule language for applications in product
configuration.
In Proceedings of the First International Workshop on Practical
Aspects of Declarative Languages, pages 305319, San Antonio, Texas,
January 1999. SpringerVerlag.
 26

T. Soininen, I. Niemelä, J. Tiihonen, and R. Sulonen.
Unified configuration knowledge representation using weight
constraint rules.
In Workshop Notes of the ECAI'2000 Configuration Workshop,
pages 7984, Berlin, Germany, August 2000.
 27

T. Soininen, I. Niemelä, J. Tiihonen, and R. Sulonen.
Representing configuration knowledge with weight constraint rules.
In Proceedings of the AAAI Spring 2001 Symposium on Answer Set
Programming, pages 195201, Stanford, USA, March 2001. AAAI Press.
 28

T. Syrjänen.
Including diagnostic information in configuration models.
In Proceedings of the First International Conference on
Computational Logic, Automated Deduction: Putting Theory into Practice,
pages 837851, London, U.K., July 2000. SpringerVerlag.
 29

T. Syrjänen.
Optimizing configurations.
In Workshop Notes of the ECAI'2000 Configuration Workshop,
pages 8590, Berlin, Germany, August 2000.
 30

T. Syrjänen.
Omegarestricted logic programs.
In Proceedings of the 6th International Conference on Logic
Programming and Nonmonotonic Reasoning, pages 267279, Vienna, Austria,
September 2001. SpringerVerlag.
 31

T. Syrjänen and I. Niemelä.
The Smodels systems.
In Proceedings of the 6th International Conference on Logic
Programming and Nonmonotonic Reasoning, pages 434438, Vienna, Austria,
September 2001. SpringerVerlag.
 32

H. Beaver and I. Niemelä.
Finding MAPs for belief networks using rulebased constraint
programming.
In Arpakannus 1/99  Special Issue on Networks'99, Espoo,
Finland, Aug 1999. Finnish Articial Intelligence Society.
Available in electronic form at
http://www.mlab.uiah.fi/networks99/.
 33

P. Simons.
Extending and implementing the stable model semantics.
Doctoral Dissertation. Research report A58, Helsinki University of
Technology, Laboratory for Theoretical Computer Science, Helsinki, Finland,
April 2000.
 34

T. Jussila.
Bounded model checking for verifying concurrent programs.
Licentiate's Thesis, Helsinki University of Technology, Department of
Computer Science and Engineering, 2001.
 35

G. Brewka and I. Niemelä.
Report on the Seventh International Workshop on Nonmonotonic
Reasoning.
AI Magazine, 19(4):139, 1998.
 36

Nisse Husberg, Tomi Janhunen, and Ilkka Niemelä (Eds.).
Leksa Notes in Computer Science, festschrift in honour of professor
Leo Ojala.
Research Report A63, Helsinki University of Technology, Laboratory
for Theoretical Computer Science, Espoo, Finland, October 2000.
 37

Jürgen Dix, Ulrich Furbach, and Ilkka Niemelä.
Nonmonotonic Reasoning: Towards Efficient Calculi and
Implementations.
Fachbericht Informatik 2098, Universität KoblenzLandau,
August 1998.
Available at
http://www.unikoblenz.de/fb4/publikationen/gelbereihe/.
 38

J. Esparza and K. Heljanko.
Implementing LTL model checking with net unfoldings.
Research Report A68, Helsinki University of Technology, Laboratory
for Theoretical Computer Science, Espoo, Finland, March 2001.
 39

K. Heljanko, V. Khomenko, and M. Koutny.
Parallelisation of the Petri net unfolding algorithm.
Technical Report CSTR733, Department of Computer Science,
University of Newcastle upon Tyne, June 2001.
 40

K. Heljanko and I. Niemelä.
Petri net analysis and nonmonotonic reasoning.
In Nisse Husberg, Tomi Janhunen, and Ilkka Niemelä, editors, Leksa Notes in Computer Science, Festschrift in Honour of Professor Leo
Ojala, pages 719. Helsinki University of Technology, Laboratory for
Theoretical Computer Science, 2000.
 41

I. Niemelä.
Automating default reasoning.
Lecture notes for a course given at the 11th European Summer School
in Logic, Language and Information, Utrecht University, Aug 1620, 1999. 25
pages. Available at http://www.tcs.hut.fi/~ini/, 1999.
 42

I. Niemelä.
Stable model semantics: From theory to implementations and
applications.
Lecture notes for a tutorial given at the First International
Conference on Computational Logic, Imperial College, London, UK, July 2428,
2000. 72 pages. Available at http://www.tcs.hut.fi/~ini/, 2000.
 43

I. Niemelä and M. Truszczynski.
Practical tools for knowledge representation and nonmonotonic
reasoning.
Lecture notes for a tutorial given at the 17th National Conference on
Artificial Intelligence, Austin, Texas, July 30August 3, 2000. 166 pages.
Available at http://www.tcs.hut.fi/~ini/, 2000.
 44

T. Soininen, I. Niemelä, J. Tiihonen, and R. Sulonen.
Unified configuration knowledge representation using weight
constraint rules.
Technical Report TKOB149, Helsinki University of Technology,
Laboratory of Information Processing Science, Helsinki, Finland, 2000.
 45

T. Syrjänen.
Implementation of local grounding for logic programs with stable
model semantics.
Technical Report B18, Helsinki University of Technology, Laboratory
for Theoretical Computer Science, Helsinki, Finland, December 1998.
 46

T. Syrjänen.
A rulebased formal model for software configuration.
Research Report A55, Helsinki University of Technology, Laboratory
for Theoretical Computer Science, Helsinki, Finland, December 1999.
 47

T. Syrjänen.
Modelling the game of life using logic programs.
In Nisse Husberg, Tomi Janhunen, and Ilkka Niemelä, editors, Leksa Notes in Computer Science, Festschrift in Honour of Professor Leo
Ojala, pages 115124. Helsinki University of Technology, Laboratory for
Theoretical Computer Science, 2000.
 48

Tommi Syrjänen.
Version spaces and rulebased configuration management.
In Working Notes of the IJCAI 2001 Workshop on Configuration,
pages 7884, August 2001.