Helsinki University of Technology, Laboratory for Theoretical Computer Science

Constraint Programming Based on Default Rules

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. Jia-Huai You, University of Alberta, Canada, Jul-Sep, 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 rule-based reasoning have been studied extensively [1,2,5,13,14,15,16,17]. Our implementation of rule-based 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 rule-based 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

Software

Bibliography

1
S. Brass, J. Dix, I. Niemelä, and T.C. Przymusinski.
On the equivalence of the static and disjunctive well-founded semantics and its computation.
Theoretical Computer Science, 258(1-2):523-553, May 2001.

2
Tomi Janhunen.
On the intertranslatability of non-monotonic logics.
Annals of Mathematics in Artificial Intelligence, 27(1-4):79-128, 1999.

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

4
P. Simons, I. Niemelä, and T. Soininen.
Extending and implementing the stable model semantics.
Artificial Intelligence, 138(1-2):181-234, 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 1241-1354. Elsevier Science, Amsterdam, 2001.

6
I. Niemelä and P. Simons.
Extending the Smodels system with cardinality and weight constraints.
In Jack Minker, editor, Logic-Based Artificial Intelligence, chapter 21, pages 491-521. 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 37-56, 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 218-232, 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 371-385, 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 90-96, 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 200-212, Vienna, Austria, September 2001. Springer-Verlag.

12
M. Hietalahti, F. Massacci, and I. Niemelä.
DES: a challenge problem for nonmonotonic reasoning systems.
In Proceedings of the 8th International Workshop on Non-Monotonic 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 216-232, Dagstuhl, Germany, October 1998. Springer-Verlag.
LNAI 1489.

14
Tomi Janhunen.
Classifying semi-normal 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 Non-Monotonic Reasoning, LPNMR'99, pages 19-33, El Paso, Texas, December 1999. Springer-Verlag.
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 852-866, London, UK, July 2000. Springer-Verlag.
LNAI 1861.

16
Tomi Janhunen.
Capturing stationary and regular extensions with Reiter's extensions.
In Ojeda-Aciego M. et al., editors, Logics in Artificial Intelligence, European Workshop, JELIA 2000, pages 102-117, Málaga, Spain, September/October 2000. Springer-Verlag.
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 93-106, 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 411-419, 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 553-567, London, U.K., July 2000. Springer-Verlag.

20
I. Niemelä.
On the complexity of dynamic constraint satisfaction.
In Proceedings of the FLoC Workshop on Complexity-Theoretic and Recursion-Theoretic Methods in Databases, Artificial Intelligence and Finite Model Theory, pages 38-47, 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 Non-Monotonic 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 317-331, El Paso, Texas, USA, December 1999. Springer-Verlag.

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 305-316, El Paso, Texas, USA, December 1999. Springer-Verlag.

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 419-433, Alexandria, Virginia, USA, October 1999. Springer-Verlag.

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 305-319, San Antonio, Texas, January 1999. Springer-Verlag.

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 79-84, 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 195-201, 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 837-851, London, U.K., July 2000. Springer-Verlag.

29
T. Syrjänen.
Optimizing configurations.
In Workshop Notes of the ECAI'2000 Configuration Workshop, pages 85-90, Berlin, Germany, August 2000.

30
T. Syrjänen.
Omega-restricted logic programs.
In Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning, pages 267-279, Vienna, Austria, September 2001. Springer-Verlag.

31
T. Syrjänen and I. Niemelä.
The Smodels systems.
In Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning, pages 434-438, Vienna, Austria, September 2001. Springer-Verlag.

32
H. Beaver and I. Niemelä.
Finding MAPs for belief networks using rule-based 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 20-98, Universität Koblenz-Landau, August 1998.
Available at http://www.uni-koblenz.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 CS-TR-733, 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 7-19. 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 16-20, 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 24-28, 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 30-August 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 TKO-B149, 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 rule-based 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 115-124. Helsinki University of Technology, Laboratory for Theoretical Computer Science, 2000.

48
Tommi Syrjänen.
Version spaces and rule-based configuration management.
In Working Notes of the IJCAI 2001 Workshop on Configuration, pages 78-84, August 2001.