×

zbMATH — the first resource for mathematics

Extending and implementing the stable model semantics. (English) Zbl 0995.68021
Summary: A novel logic program like language, weight constraint rules, is developed for answer set programming purposes. It generalizes normal logic programs by allowing weight constraints in place of literals to represent, e.g., cardinality and resource constraints and by providing optimization capabilities. A declarative semantics is developed which extends the stable model semantics of normal programs. The computational complexity of the language is shown to be similar to that of normal programs under the stable model semantics. A simple embedding of general weight constraint rules to a small subclass of the language called basic constraint rules is devised. An implementation of the language, the \(s\)-models system, is developed based on this embedding. It uses a two level architecture consisting of a front-end and a kernel language implementation.
The front-end allows restricted use of variables and functions and compiles general weight constraint rules to basic constraint rules. A major part of the work is the development of an efficient search procedure for computing stable models for this kernel language. The procedure is compared with and empirically tested against satisfiability checkers and an implementation of the stable model semantics. It offers a competitive implementation of the stable model semantics for normal programs and attractive performance for problems where the new types of rules provide a compact representation.

MSC:
68N17 Logic programming
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aiello, L.C.; Massacci, F., Verifying security protocols as planning in logic programming, ACM trans. comput. logic, 2, 4, 542-580, (2001) · Zbl 1365.68386
[2] Aura, T.; Bishop, M.; Sniegowski, D., Analyzing single-server network inhibition, (), 108-117
[3] Bell, C.; Nerode, A.; Ng, R.T.; Subrahmanian, V.S., Mixed integer programming methods for computing nonmonotonic deductive databases, J. ACM, 41, 6, 1178-1215, (1994) · Zbl 0830.68039
[4] Ben-Eliyahu, R.; Dechter, R., Default reasoning using classical logic, Artificial intelligence, 84, 113-150, (1996)
[5] Buccafurri, F.; Leone, N.; Rullo, P., Strong and weak constraints in disjunctive Datalog, (), 2-17
[6] Cadoli, M.; Palopoli, L.; Schaerf, A.; Vasile, D., NP-SPEC: an executable specification language for solving all problems in NP, (), 16-30
[7] Chen, W.; Warren, D.S., Computation of stable models and its integration with logical query processing, IEEE trans. knowledge data engrg., 8, 5, 742-757, (1996)
[8] Cholewiński, P.; Marek, V.W.; Mikitiuk, A.; Truszczyński, M., Computing with default logic, Artificial intelligence, 112, 105-146, (1999) · Zbl 0996.68195
[9] Crawford, J.M.; Auton, L.D., Experimental results on the crossover point in random 3-SAT, Artificial intelligence, 81, 1, 31-57, (1996)
[10] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem proving, Comm. ACM, 5, 394-397, (1962) · Zbl 0217.54002
[11] de Kleer, J., An assumption-based TMS, Artificial intelligence, 28, 127-162, (1986)
[12] Dimopoulos, Y., On computing logic programs, J. automat. reason., 17, 259-289, (1996) · Zbl 0865.68026
[13] Dimopoulos, Y.; Nebel, B.; Koehler, J., Encoding planning problems in non-monotonic logic programs, (), 169-181
[14] Dowling, W.F.; Gallier, J.H., Linear-time algorithms for testing the satisfiability of propositional Horn formulae, J. logic programming, 3, 267-284, (1984) · Zbl 0593.68062
[15] Doyle, J., A truth maintenance system, Artificial intelligence, 12, 231-272, (1979)
[16] East, D.; Truszczyński, M., DATALOG with constraints—an answer-set programming system, (), 163-168
[17] Eiter, T.; Gottlob, G., On the computational cost of disjunctive logic programming: propositional case, Ann. math. artificial intelligence, 15, 289-323, (1995) · Zbl 0858.68016
[18] Eiter, T.; Gottlob, G.; Mannila, H., Disjunctive Datalog, ACM trans. database systems, 22, 3, 364-418, (1997)
[19] Elkan, C., A rational reconstruction of nonmonotonic truth maintenance systems, Artificial intelligence, 43, 219-234, (1990) · Zbl 0717.68081
[20] Eshghi, K., Computing stable models by using the ATMS, (), 272-277
[21] Faber, W.; Leone, N.; Pfeifer, G., Pushing goal derivation in DLP computations, (), 177-191
[22] Faber, W.; Leone, N.; Pfeifer, G., Optimizing the computation of heuristics for answer set programming systems, (), 295-308 · Zbl 1010.68533
[23] Freeman, J.W., Improvements to propositional satisfiability search algorithms, ph.D. thesis, (1995), University of Pennsylvania
[24] Gelfond, M.; Lifschitz, V., The stable model semantics for logic programming, (), 1070-1080
[25] Greco, S., Dynamic programming in Datalog with aggregates, IEEE trans. knowledge data engrg., 11, 2, 265-283, (1999)
[26] Heljanko, K., Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets, Fund. inform., 37, 3, 247-268, (1999) · Zbl 0930.68096
[27] Hietalahti, M.; Massacci, F.; Niemelä, I., DES: A challenge problem for nonmonotonic reasoning systems, (), cs.AI/0003039
[28] D.E. Knuth, The Stanford GraphBase, 1993. Available at ftp://labrea.stanford.edu/ · Zbl 0806.68121
[29] Krentel, M., The complexity of optimization problems, J. comput. system sci., 36, 490-509, (1988) · Zbl 0652.68040
[30] Leone, N., Dlv, release 2001-06-11, 2001. A Disjunctive Datalog System
[31] Leone, N.; Romeo, M.; Rullo, P.; Saccà, D., Effective implementation of negation in database logic query languages, (), 159-175
[32] Leone, N.; Rullo, L.; Scarcello, F., Disjunctive stable models: unfounded sets, fixpoint semantics, and computation, Inform. and comput., 135, 2, 69-112, (1997) · Zbl 0879.68019
[33] Li, C.M., A constraint-based approach to narrow search trees for satisfiability, Inform. process. lett., 71, 75-80, (1999) · Zbl 1015.68518
[34] Li, C.M.; Anbulagan, Look-ahead versus look-back for satisfiability problems, (), 341-355
[35] Lifschitz, V., On the declarative semantics of logic programs with negation, (), 177-192 · Zbl 0718.68019
[36] Lifschitz, V., Answer set planning, (), 25-37
[37] Lifschitz, V.; Woo, T.Y.C., Answer sets in general nonmonotonic reasoning (preliminary report), (), 603-614
[38] Liu, X.; Ramakrishnan, C.R.; Smolka, S.A., Fully local and efficient evaluation of alternating fixed points, (), 5-19
[39] Marek, V.W.; Subrahmanian, V.S., The relationship between stable, supported, default and autoepistemic semantics for general logic programs, Theoret. comput. sci., 103, 2, 365-386, (1992) · Zbl 0753.68062
[40] Marek, V.W.; Truszczyński, M., Stable models and an alternative logic programming paradigm, (), 375-398, cs.LO/9809032 · Zbl 0979.68524
[41] McCarthy, J., Circumscription—A form of non-monotonic reasoning, Artificial intelligence, 13, 27-39, (1980) · Zbl 0435.68073
[42] McCarthy, J., Applications of circumscription to formalizing commonsense knowledge, Artificial intelligence, 28, 89-116, (1986)
[43] Moore, R.C., Semantical considerations on nonmonotonic logic, Artificial intelligence, 25, 75-94, (1985) · Zbl 0569.68079
[44] Niemelä, I., Logic programming with stable model semantics as a constraint programming paradigm, Ann. math. artificial intelligence, 25, 3-4, 241-273, (1999) · Zbl 0940.68018
[45] Niemelä, I.; Simons, P., Extending the smodels system with cardinality and weight constraints, (), 491-521, Chapter 21 · Zbl 0979.68015
[46] Niemelä, I.; Simons, P.; Soininen, T., Stable model semantics of weight constraint rules, (), 317-331 · Zbl 0952.68029
[47] Papadimitriou, C.H., Computational complexity, (1995), Addison-Wesley Reading, MA · Zbl 0557.68033
[48] Pimentel, S.G.; Rodi, W.L., A nonmonotonic assumption-based TMS using stable bases, (), 485-495 · Zbl 0765.68199
[49] Przymusinski, T., Stable semantics for disjunctive programs, New generation computing, 9, 3-4, 401-424, (1991) · Zbl 0796.68053
[50] Reiter, R., A logic for default reasoning, Artificial intelligence, 13, 81-132, (1980) · Zbl 0435.68069
[51] Rintanen, J., Lexicographic priorities in default logic, Artificial intelligence, 106, 221-265, (1998) · Zbl 0910.68162
[52] Sakama, C.; Inoue, K., An alternative approach to the semantics of disjunctive logic programs and deductive databases, J. automat. reason., 13, 145-172, (1994) · Zbl 0819.68036
[53] Sakama, C.; Inoue, K., Representing priorities in logic programs, (), 82-96
[54] B. Selman, Random k-SAT generator, 1994. Available at ftp://ftp.research.att.com/dist/ai/makewff.sh.Z
[55] Simons, P., Extending the stable model semantics with more expressive rules, (), 305-316 · Zbl 0952.68028
[56] Simons, P., Extending and implementing the stable model semantics, doctoral dissertation, research report A58, (2000), Helsinki University of Technology Helsinki, Finland
[57] Simons, P., Smodels 2.26, 2000. A system for computing the stable models of logic programs
[58] Soininen, T.; Gelle, E.; Niemelä, I., A fixpoint definition of dynamic constraint satisfaction, (), 419-433
[59] Soininen, T.; Niemelä, I., Developing a declarative rule language for applications in product configuration, (), 305-319
[60] Soininen, T.; Niemelä, I.; Tiihonen, J.; Sulonen, R., Representing configuration knowledge with weight constraint rules, (), 195-201
[61] Subrahmanian, V.S.; Nau, D.; Vago, C., WFS + branch and bound = stable models, IEEE trans. knowledge data engrg., 7, 3, 362-377, (1995)
[62] Syrjänen, T., Including diagnostic information in configuration models, (), 837-851 · Zbl 0983.68653
[63] Syrjänen, T., Lparse, a procedure for grounding domain-restricted logic programs, 2001
[64] Syrjänen, T., Omega-restricted programs, (), 267-279 · Zbl 1007.68503
[65] Truszczynski, M., Deres, a default reasoning system, 1999
[66] Van Gelder, A.; Ross, K.A.; Schlipf, J.S., The well-founded semantics for general logic programs, J. ACM, 38, 3, 620-650, (1991) · Zbl 0799.68045
[67] Warren, D.S., The XSB programming system, 2000
[68] Zabih, R.; McAllester, D., A rearrangement search strategy for determining propositional satisfiability, (), 155-160
[69] Zaniolo, C., LDL^++, a second-generation deductive database system, 1999
[70] Zhang, H., SATO: an efficient propositional prover, (), 272-275
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.