{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,20]],"date-time":"2023-11-20T13:34:50Z","timestamp":1700487290896},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"6","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[1994,11]]},"abstract":"Though the declarative semantics of both explicit and nonmonotonic negation in logic programs has been studied extensively, relatively little work has been done on computation and implementation of these semantics. In this paper, we study three different approaches to computing stable models of logic programs based on mixed integer linear programming methods for automated deduction introduced by R. Jeroslow. We subsequently discuss the relative efficiency of these algorithms. The results of experiments with a prototype compiler implemented by us tend to confirm our theoretical discussion. In contrast to resolution, the mixed integer programming methodology is both fully declarative and handles reuse of old computations gracefully.<\/jats:p>\n We also introduce, compare, implement, and experiment with linear constraints corresponding to four semantics for \u201cexplicit\u201d negation in logic programs: the four-valued annotated semantics [Blair and Subrahmanian 1989], the Gelfond-Lifschitz semantics [1990], the over-determined models [Grant and Subrahmanian 1989], the Gelfond-Lifschitz semantics [1990], the over-determined models [Grant and Subrahmanian 1990], and the classical logic semantics. Gelfond and Lifschitz[1990] argue for simultaneous use of two modes of negation in logic programs, \u201cclassical\u201d and \u201cnonmonotonic,\u201d so we give algorithms for computing \u201canswer sets\u201d for such logic programs too.<\/jats:p>","DOI":"10.1145\/195613.195637","type":"journal-article","created":{"date-parts":[[2002,7,27]],"date-time":"2002-07-27T11:25:57Z","timestamp":1027769157000},"page":"1178-1215","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":52,"title":["Mixed integer programming methods for computing nonmonotonic deductive databases"],"prefix":"10.1145","volume":"41","author":[{"given":"Colin","family":"Bell","sequence":"first","affiliation":[{"name":"Univ. of Iowa, Iowa City"}]},{"given":"Anil","family":"Nerode","sequence":"additional","affiliation":[{"name":"Cornell Univ., Ithaca, NY"}]},{"given":"Raymond T.","family":"Ng","sequence":"additional","affiliation":[{"name":"Univ. of British Columbia, Vancouver, B. C., Canada"}]},{"given":"V. S.","family":"Subrahmanian","sequence":"additional","affiliation":[{"name":"Univ. of Maryland, College Park"}]}],"member":"320","published-online":{"date-parts":[[1994,11]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"283","volume-title":"Proceedblgs of the l lth ACM SIG,4CT-SIGMOD-SIG~4RT ~Symposium on Principles of Database &'stems (San Diego, Calif., June 2-4). ACM","author":"~BELL C.","unstructured":"~BELL , C. , NERODE , A. , NO , R. , AND SUBRAHMANI a, N, V S. 1992. Implementing deductive ~databases by linear programming . In Proceedblgs of the l lth ACM SIG,4CT-SIGMOD-SIG~4RT ~Symposium on Principles of Database &'stems (San Diego, Calif., June 2-4). ACM , New York , ~pp. 283 - 292 . ( Currently available as Tech. Rep. CS-TR-2747. Univ. Maryland, College Park, ~Md., (Aug.) 1991.) 10.1145\/137097.137892 ~BELL, C., NERODE, A., NO, R., AND SUBRAHMANIa, N, V S. 1992. Implementing deductive ~databases by linear programming. In Proceedblgs of the l lth ACM SIG,4CT-SIGMOD-SIG~4RT ~Symposium on Principles of Database &'stems (San Diego, Calif., June 2-4). ACM, New York, ~pp. 283-292. (Currently available as Tech. Rep. CS-TR-2747. Univ. Maryland, College Park, ~Md., (Aug.) 1991.) 10.1145\/137097.137892"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"~BLAIR C. JEROSLOW R G. AND LOWE J. K. 1988. Some results and experiments m program- ~ming techniques for propositional logic. Cottz{;tit. Op. Re5 13 633 645. 10.1016\/0305-0548(86)90056-0 ~BLAIR C. JEROSLOW R G. AND LOWE J. K. 1988. Some results and experiments m program- ~ming techniques for propositional logic. Cottz{;tit. Op. Re5 13 633 645. 10.1016\/0305-0548(86)90056-0","DOI":"10.1016\/0305-0548(86)90056-0"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90126-6"},{"key":"e_1_2_1_4_1","first-page":"274","volume-title":"A truth maintenance system based on stable models. In ~Proceedbzgs of the 1989 North American Conference on Logic Programming","author":"~CUADRADO J.","unstructured":"~CUADRADO , J. , AND PiME NTEL , S. 1989. A truth maintenance system based on stable models. In ~Proceedbzgs of the 1989 North American Conference on Logic Programming , MIT Press , Cam- ~bridge, Mass. pp. 274 - 290 . ~CUADRADO, J., AND PiMENTEL, S. 1989. A truth maintenance system based on stable models. In ~Proceedbzgs of the 1989 North American Conference on Logic Programming, MIT Press, Cam- ~bridge, Mass. pp. 274-290."},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","article-title":"Linear-time algorithms for testing the satlsfiabdlty of ~propositional horn theories","volume":"3","author":"~DOWLING W.","year":"1984","unstructured":"~DOWLING , W. , AND GALLIER , J. 1984 . Linear-time algorithms for testing the satlsfiabdlty of ~propositional horn theories . J. Logic Prog. 3 , 267 284. ~DOWLING, W., AND GALLIER, J. 1984. Linear-time algorithms for testing the satlsfiabdlty of ~propositional horn theories. J. Logic Prog. 3, 267 284.","journal-title":"J. Logic Prog."},{"key":"e_1_2_1_6_1","first-page":"449","article-title":"Disjunctive LP + Integrity ~constraints - Stable model semantics. ,4n~l","volume":"18","author":"~FERNANDEZ J.","year":"1993","unstructured":"~FERNANDEZ , J. , LOBO , J. , MINKER , J. , AND SUBRAHMANIAN , V. S. 1993 . Disjunctive LP + Integrity ~constraints - Stable model semantics. ,4n~l . Math. Artlf. Int. 18 , 449 479. ~FERNANDEZ, J., LOBO, J., MINKER, J., AND SUBRAHMANIAN, V. S. 1993. Disjunctive LP + Integrity ~constraints - Stable model semantics. ,4n~l. Math. Artlf. Int. 18, 449 479.","journal-title":"Math. Artlf. Int."},{"key":"e_1_2_1_7_1","unstructured":"~FUENI'ES L. O. 1991. Applying uncertainty formalisms to well-defined problems manuscript ~FUENI'ES L. O. 1991. Applying uncertainty formalisms to well-defined problems manuscript"},{"key":"e_1_2_1_8_1","first-page":"1070","volume-title":"V 1988. The stable model semantics for logic programming. In ~Proceedings of the 5th InternattorzaI Conference and Symposzum on Logtc Programming (R. A. ~Kowalski and K. A. Bowen, ed.).","author":"~GELFOND M.","unstructured":"~GELFOND , M. , AND LIFSCH 1 TZ , V 1988. The stable model semantics for logic programming. In ~Proceedings of the 5th InternattorzaI Conference and Symposzum on Logtc Programming (R. A. ~Kowalski and K. A. Bowen, ed.). pp. 1070 - 1080 . ~GELFOND, M., AND LIFSCH1TZ, V 1988. The stable model semantics for logic programming. In ~Proceedings of the 5th InternattorzaI Conference and Symposzum on Logtc Programming (R. A. ~Kowalski and K. A. Bowen, ed.). pp. 1070-1080."},{"key":"e_1_2_1_9_1","first-page":"579","volume-title":"Proceedings of ~the 7th Internattonal Conference and &,rnposiztm on Logic Programming (D. H. D. Warren and ~P. Szeredl, eds.)","author":"ELFOND M.","year":"1990","unstructured":"~(3 ELFOND , M. , AND LIFSCHITZ , V. 1990 . Logic programs with classical negation . In Proceedings of ~the 7th Internattonal Conference and &,rnposiztm on Logic Programming (D. H. D. Warren and ~P. Szeredl, eds.) , pp. 579 - 597 . ~(3ELFOND, M., AND LIFSCHITZ, V. 1990. Logic programs with classical negation. In Proceedings of ~the 7th Internattonal Conference and &,rnposiztm on Logic Programming (D. H. D. Warren and ~P. Szeredl, eds.), pp. 579-597."},{"key":"e_1_2_1_10_1","volume-title":"Introduction to Operations Research: ~4 Comp,ter-Ortentcd Algorithmtc ~Approach","author":"~GILLET B. E.","unstructured":"~GILLET , B. E. 1976. Introduction to Operations Research: ~4 Comp,ter-Ortentcd Algorithmtc ~Approach . McGraw-Hill , New York . ~GILLET, B. E. 1976. Introduction to Operations Research: ~4 Comp,ter-Ortentcd Algorithmtc ~Approach. McGraw-Hill, New York."},{"key":"e_1_2_1_11_1","volume-title":"Rece~ztAdt'aHce,s ~m Mathematical Programming","author":"~GOMORY R. E.","unstructured":"~GOMORY , R. E. 1963. An algorithm for integer solutions to hnear programs . In Rece~ztAdt'aHce,s ~m Mathematical Programming (R. Graves and P. Wolfe, eds.). McGraw-Hill , New York . ~GOMORY, R. E. 1963. An algorithm for integer solutions to hnear programs. In Rece~ztAdt'aHce,s ~m Mathematical Programming (R. Graves and P. Wolfe, eds.). McGraw-Hill, New York."},{"key":"e_1_2_1_12_1","volume-title":"g. S","author":"~GRANT J.","year":"1990","unstructured":"~GRANT , J. , AND SUBRAHMANIAN , g. S . 1990 . Reasoning about inconsistent knowledge bases. ~IEEE Tra~zs. Ktzow. Data Eng ., to appear. (Currently available as Tech. Rep. CS-TR-2532. Unw. ~Maryland, College Park, Md.) ~GRANT, J., AND SUBRAHMANIAN, g. S. 1990. Reasoning about inconsistent knowledge bases. ~IEEE Tra~zs. Ktzow. Data Eng., to appear. (Currently available as Tech. Rep. CS-TR-2532. Unw. ~Maryland, College Park, Md.)"},{"key":"e_1_2_1_13_1","volume-title":"i986. ltztrodttetton to Operations Researrh","author":"~H ER, F","unstructured":"~H 1LL1 ER, F ., AND LIEBERMAN , G. i986. ltztrodttetton to Operations Researrh , 4 th ed Holden-Day, ~Oakland, Cahf . ~H1LL1ER, F., AND LIEBERMAN, G. i986. ltztrodttetton to Operations Researrh, 4th ed Holden-Day, ~Oakland, Cahf.","edition":"4"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"~HOOKER J. 1988. A quantitative approach to logical inference. Dec. Supp. Syst. 4 45-69. 10.1016\/0167-9236(88)90097-8 ~HOOKER J. 1988. A quantitative approach to logical inference. Dec. Supp. Syst. 4 45-69. 10.1016\/0167-9236(88)90097-8","DOI":"10.1016\/0167-9236(88)90097-8"},{"key":"e_1_2_1_15_1","first-page":"123","article-title":"Branch-and-cut solution of inference problems in proposi- ~tional logic","author":"~HOOKER J.","year":"1990","unstructured":"~HOOKER , J. , AND FEDJK 1, C. 1990 . Branch-and-cut solution of inference problems in proposi- ~tional logic . Ann. Math. Artif Int. , 123 - 139 . ~HOOKER, J., AND FEDJK1, C. 1990. Branch-and-cut solution of inference problems in proposi- ~tional logic. Ann. Math. Artif Int., 123-139.","journal-title":"Ann. Math. Artif Int."},{"key":"e_1_2_1_16_1","first-page":"111","volume-title":"Proceedings of the 14th ~Annual Symposium on Principles of Programming Languages.","author":"~JAFFAR J.","year":"1987","unstructured":"~JAFFAR , J. , AND LASSEZ , J. L. 1987 . Constraint logic programming . In Proceedings of the 14th ~Annual Symposium on Principles of Programming Languages. ( Munich, West Germany, Jan. ~21-23). ACM, New York , pp. 111 - 119 . 10.1145\/41625.41635 ~JAFFAR, J., AND LASSEZ, J. L. 1987. Constraint logic programming. In Proceedings of the 14th ~Annual Symposium on Principles of Programming Languages. (Munich, West Germany, Jan. ~21-23). ACM, New York, pp. 111-119. 10.1145\/41625.41635"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-9236(88)90128-5"},{"key":"e_1_2_1_18_1","volume-title":"Logic-based Decision Support: Mixed Integer Model Formulation. North- ~Holland","author":"~JEROSLOW R. E.","unstructured":"~JEROSLOW , R. E. 1989. Logic-based Decision Support: Mixed Integer Model Formulation. North- ~Holland , Amsterdam, The Netherlands . ~JEROSLOW, R. E. 1989. Logic-based Decision Support: Mixed Integer Model Formulation. North- ~Holland, Amsterdam, The Netherlands."},{"key":"e_1_2_1_19_1","unstructured":"~KAGAN V. NERODE A. AND SUBRAHMANIAN V. S. 1993. Computing definite logic programs by ~partial instantiation. Math. Sciences Inst. TR-93-24. Cornell Univ. Ithaca N.Y. May. ~KAGAN V. NERODE A. AND SUBRAHMANIAN V. S. 1993. Computing definite logic programs by ~partial instantiation. Math. Sciences Inst. TR-93-24. Cornell Univ. Ithaca N.Y. May."},{"key":"e_1_2_1_20_1","unstructured":"~KAGAN V. NERODE A. AND SUBRAHMANIAN V. S. 1994. Computing minimal models by partial ~instantiation. Theoret. Conzpttt. Sci. to appear. 10.1016\/0304-3975(94)00216-9 ~KAGAN V. NERODE A. AND SUBRAHMANIAN V. S. 1994. Computing minimal models by partial ~instantiation. Theoret. Conzpttt. Sci. to appear. 10.1016\/0304-3975(94)00216-9"},{"key":"e_1_2_1_21_1","unstructured":"~KHACmAN L. G. 1979. A polynomial algorithm for linear programming. Doklady Akad. Nauk ~USSR 224 1093-1096. (Translated in Soviet Math Doklady 20 191-194.) ~KHACmAN L. G. 1979. A polynomial algorithm for linear programming. Doklady Akad. Nauk ~USSR 224 1093-1096. (Translated in Soviet Math Doklady 20 191-194.)"},{"key":"e_1_2_1_22_1","volume-title":"Foundations of Logic Programming","author":"~LLOYD J. W.","unstructured":"~LLOYD , J. W. 1987. Foundations of Logic Programming . Springer-Verlag , New York . ~LLOYD, J. W. 1987. Foundations of Logic Programming. Springer-Verlag, New York."},{"key":"e_1_2_1_23_1","volume-title":"Foundations of Disjuncttt,e Logic' Programming, ~MIT Press","author":"~LOBO J.","unstructured":"~LOBO , J. , MINKER , J. , AND RAJASEKAR , A. 1992. Foundations of Disjuncttt,e Logic' Programming, ~MIT Press , Cambridge , Mass . ~LOBO, J., MINKER, J., AND RAJASEKAR, A. 1992. Foundations of Disjuncttt,e Logic' Programming, ~MIT Press, Cambridge, Mass."},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"~MAREK W. NERODE A. AND REMMEL J. 1991. A theory of nonmonotonic rule systems I. Ann. ~Math. Arti. hzt. 1 241-273. ~MAREK W. NERODE A. AND REMMEL J. 1991. A theory of nonmonotonic rule systems I. Ann. ~Math. Arti. hzt. 1 241-273.","DOI":"10.1007\/BF01531080"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90019-C"},{"key":"e_1_2_1_26_1","first-page":"292","volume-title":"Proceedings of the ~6th Con)'~rence on Automated Deduction, (D. Loveland, ed.). Lecture Notes in Computer ~Science","volume":"138","author":"~MINKER J.","year":"1982","unstructured":"~MINKER , J. 1982 . On indefinite databases and the closed world assumption . In Proceedings of the ~6th Con)'~rence on Automated Deduction, (D. Loveland, ed.). Lecture Notes in Computer ~Science , vol. 138 . Springer-Verlag, New York , pp. 292 - 308 . ~MINKER, J. 1982. On indefinite databases and the closed world assumption. In Proceedings of the ~6th Con)'~rence on Automated Deduction, (D. Loveland, ed.). Lecture Notes in Computer ~Science, vol. 138. Springer-Verlag, New York, pp. 292-308."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.91059"},{"key":"e_1_2_1_28_1","volume-title":"Integer and Combinatorial Optimization","author":"~NEMHAUSER G.","unstructured":"~NEMHAUSER , G. , AND WOLSEY , L. 1988. Integer and Combinatorial Optimization . Wiley , New ~York. ~NEMHAUSER, G., AND WOLSEY, L. 1988. Integer and Combinatorial Optimization. Wiley, New ~York."},{"issue":"2","key":"e_1_2_1_29_1","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1109\/21.31034","article-title":"A connectionist model for diagnostic problem solving. IEEE ~Trans","volume":"19","author":"~PENG Y.","year":"1989","unstructured":"~PENG , Y. , AND REGGIA , J. 1989 . A connectionist model for diagnostic problem solving. IEEE ~Trans . Syst., Man and Cyber. 19 , 2 , 285 - 298 . ~PENG, Y., AND REGGIA, J. 1989. A connectionist model for diagnostic problem solving. IEEE ~Trans. Syst., Man and Cyber. 19, 2, 285-298.","journal-title":"Syst., Man and Cyber."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.390244"},{"key":"e_1_2_1_31_1","volume-title":"Principles of Database and Knowledge-Base System","author":"~ULLMAN J. D.","unstructured":"~ULLMAN , J. D. 1988. Principles of Database and Knowledge-Base System . Vol. 1 . Computer ~Science Press, Baltimore, Md . ~ULLMAN, J. D. 1988. Principles of Database and Knowledge-Base System. Vol. 1. Computer ~Science Press, Baltimore, Md."},{"key":"e_1_2_1_32_1","first-page":"1","volume-title":"Proceedings ~of the 8th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems ~","author":"~VAN GELDER A.","year":"1989","unstructured":"~VAN GELDER , A. 1989 . The alternating fixpoint of logic programs with negation . In Proceedings ~of the 8th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems ~ ( Philadelphia, Pa., Mar. 29-3t). ACM. New York , pp. 1 10. 10.1145\/73721.73722 ~VAN GELDER, A. 1989. The alternating fixpoint of logic programs with negation. In Proceedings ~of the 8th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems ~(Philadelphia, Pa., Mar. 29-3t). ACM. New York, pp. 1 10. 10.1145\/73721.73722"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/195613.195637","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T19:31:46Z","timestamp":1672342306000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/195613.195637"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,11]]},"references-count":32,"journal-issue":{"issue":"6","published-print":{"date-parts":[[1994,11]]}},"alternative-id":["10.1145\/195613.195637"],"URL":"http:\/\/dx.doi.org\/10.1145\/195613.195637","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,11]]},"assertion":[{"value":"1994-11-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}