{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:21:21Z","timestamp":1750306881376,"version":"3.41.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,2,1]],"date-time":"2013-02-01T00:00:00Z","timestamp":1359676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2013,2]]},"abstract":"<jats:p>A consequence of a logic program under answer set semantics is one that is true for all answer sets. This article considers using loop formulas to compute some of these consequences in order to increase the efficiency of answer set solvers. Since computing loop formulas are in general intractable, we consider only loops with either no external support or at most one external support, as their loop formulas are either unit or binary clauses. We show that for disjunctive logic programs, loop formulas of loops with no external support can be computed in polynomial time, and that an iterative procedure using unit propagation on these formulas and the program completion computes the well-founded models in the case of normal logic programs and the least fixed point of a simplification operator used by DLV for disjunctive logic programs. For loops with at most one external support, their loop formulas can be computed in polynomial time for normal logic programs, but are NP-hard for disjunctive programs. So for normal logic programs, we have a procedure similar to the iterative one for loops without any external support, but for disjunctive logic programs, we present a polynomial approximation algorithm. All these algorithms have been implemented, and our experiments show that for certain logic programs, the consequences computed by our algorithms can significantly speed up current ASP solvers cmodels, clasp, and DLV.<\/jats:p>","DOI":"10.1145\/2422085.2422088","type":"journal-article","created":{"date-parts":[[2013,2,22]],"date-time":"2013-02-22T19:25:04Z","timestamp":1361561104000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Computing Loops with at Most One External Support Rule"],"prefix":"10.1145","volume":"14","author":[{"given":"Xiaoping","family":"Chen","sequence":"first","affiliation":[{"name":"University of Science and Technology of China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianmin","family":"Ji","sequence":"additional","affiliation":[{"name":"University of Science and Technology of China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fangzhen","family":"Lin","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,2]]},"reference":[{"volume-title":"Proceedings of the International Workshop on NonmonotoniReasoning (NMR\u201906)","author":"Anger C.","unstructured":"Anger , C. , Gebser , M. , and Schaub , T . 2006. Approaching the core of unfounded sets . In Proceedings of the International Workshop on NonmonotoniReasoning (NMR\u201906) . 58--66. Anger, C., Gebser, M., and Schaub, T. 2006. Approaching the core of unfounded sets. In Proceedings of the International Workshop on NonmonotoniReasoning (NMR\u201906). 58--66.","key":"e_1_2_1_1_1"},{"volume-title":"Reasoning and Declarative Problem Solving","author":"Baral C.","unstructured":"Baral , C. 2003. Knowledge Representation , Reasoning and Declarative Problem Solving . Cambridge University Press . Baral, C. 2003. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press.","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","first-page":"1","article-title":"Semantics of (disjunctive) logiprograms based on partial evaluation","volume":"40","author":"Brass S.","year":"1999","unstructured":"Brass , S. and Dix , J. 1999 . Semantics of (disjunctive) logiprograms based on partial evaluation . J. LogiProgram. 40 , 1, 1 -- 46 . Brass, S. and Dix, J. 1999. Semantics of (disjunctive) logiprograms based on partial evaluation. J. LogiProgram. 40, 1, 1--46.","journal-title":"J. LogiProgram."},{"volume-title":"Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201908)","author":"Chen X.","unstructured":"Chen , X. , Ji , J. , and Lin , F . 2008. Computing loops with at most one external support rule . In Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201908) . 401--410. Chen, X., Ji, J., and Lin, F. 2008. Computing loops with at most one external support rule. In Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201908). 401--410.","key":"e_1_2_1_4_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1007\/978-3-642-02846-5_15"},{"volume-title":"Proceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201906)","author":"Chen Y.","unstructured":"Chen , Y. , Lin , F. , Wang , Y. , and Zhang , M . 2006. First-order loop formulas for normal logiprograms . In Proceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201906) . 298--307. Chen, Y., Lin, F., Wang, Y., and Zhang, M. 2006. First-order loop formulas for normal logiprograms. In Proceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201906). 298--307.","key":"e_1_2_1_6_1"},{"volume-title":"Negation as failure","author":"Clark K. L.","unstructured":"Clark , K. L. 1978. Negation as failure . In Logiand Databases, H. Gallaire and J. Minker, Eds. Plenum Press , New York, NY , 293--322. Clark, K. L. 1978. Negation as failure. In Logiand Databases, H. Gallaire and J. Minker, Eds. Plenum Press, New York, NY, 293--322.","key":"e_1_2_1_7_1"},{"volume-title":"Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201908)","author":"Drescher C.","unstructured":"Drescher , C. , Gebser , M. , Grote , T. , Kaufmann , B. , K\u00f6nig , A. , Ostrowski , M. , and Schaub , T . 2008. Conflict-driven disjunctive answer set solving . In Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201908) . 422--432. Drescher, C., Gebser, M., Grote, T., Kaufmann, B., K\u00f6nig, A., Ostrowski, M., and Schaub, T. 2008. Conflict-driven disjunctive answer set solving. In Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201908). 422--432.","key":"e_1_2_1_8_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1007\/s10472-006-9025-2"},{"volume-title":"Proceddings of the 20th International Joint Conference on Artificial Intelligence (IJCAI\u201907)","author":"Gebser M.","unstructured":"Gebser , M. , Kaufmann , B. , Neumann , A. , and Schaub , T . 2007. Conflict-driven answer set solving . In Proceddings of the 20th International Joint Conference on Artificial Intelligence (IJCAI\u201907) . 386--392. Gebser, M., Kaufmann, B., Neumann, A., and Schaub, T. 2007. Conflict-driven answer set solving. In Proceddings of the 20th International Joint Conference on Artificial Intelligence (IJCAI\u201907). 386--392.","key":"e_1_2_1_10_1"},{"volume-title":"Proceedings of the 9th International Conference on LogiProgramming and Nonmonotoni Reasoning (LPNMR\u201907)","author":"Gebser M.","unstructured":"Gebser , M. , Schaub , T. , and Thiele , S . 2007. Gringo: A new grounder for answer set programming . In Proceedings of the 9th International Conference on LogiProgramming and Nonmonotoni Reasoning (LPNMR\u201907) . 266--271. Gebser, M., Schaub, T., and Thiele, S. 2007. Gringo: A new grounder for answer set programming. In Proceedings of the 9th International Conference on LogiProgramming and Nonmonotoni Reasoning (LPNMR\u201907). 266--271.","key":"e_1_2_1_11_1"},{"volume-title":"Proceedings of the 5th International Conference on LogiProgramming (ICLP\u201988)","author":"Gelfond M.","unstructured":"Gelfond , M. and Lifschitz , V . 1988. The stable model semantics for logiprogramming . In Proceedings of the 5th International Conference on LogiProgramming (ICLP\u201988) . 1070--1080. Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logiprogramming. In Proceedings of the 5th International Conference on LogiProgramming (ICLP\u201988). 1070--1080.","key":"e_1_2_1_12_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1007\/BF03037169"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1007\/s10817-006-9033-2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.5555\/1642293.1642374"},{"volume-title":"Proceedings of the 19th International Conference on LogiProgramming (ICLP\u201903)","author":"Lee J.","unstructured":"Lee , J. and Lifschitz , V . 2003. Loop formulas for disjunctive logiprograms . In Proceedings of the 19th International Conference on LogiProgramming (ICLP\u201903) . 451--465. Lee, J. and Lifschitz, V. 2003. Loop formulas for disjunctive logiprograms. In Proceedings of the 19th International Conference on LogiProgramming (ICLP\u201903). 451--465.","key":"e_1_2_1_16_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1016\/j.artint.2005.09.003"},{"volume-title":"Proceedings of the 11th International Conference on Knowledge Representation and Reasoning (KR\u201908)","author":"Lee J.","unstructured":"Lee , J. and Meng , Y . 2008. On loop formulas with variables . In Proceedings of the 11th International Conference on Knowledge Representation and Reasoning (KR\u201908) . 444--453. Lee, J. and Meng, Y. 2008. On loop formulas with variables. In Proceedings of the 11th International Conference on Knowledge Representation and Reasoning (KR\u201908). 444--453.","key":"e_1_2_1_18_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1006\/inco.1997.2630"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1145\/1149114.1149117"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1145\/1131313.1131316"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.5555\/1622591.1622603"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1016\/j.artint.2004.04.004"},{"volume-title":"Proceedings of the 9th International Conference on LogiProgramming and NonmonotoniReasoning (LPNMR\u201907)","author":"Liu G.","unstructured":"Liu , G. and You , J . 2007. On the effectiveness of looking ahead in search for answer sets . In Proceedings of the 9th International Conference on LogiProgramming and NonmonotoniReasoning (LPNMR\u201907) . 303--308. Liu, G. and You, J. 2007. On the effectiveness of looking ahead in search for answer sets. In Proceedings of the 9th International Conference on LogiProgramming and NonmonotoniReasoning (LPNMR\u201907). 303--308.","key":"e_1_2_1_24_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1023\/A:1018930122475"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1016\/S0004-3702(02)00187-X"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1145\/73721.73722"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1145\/116825.116838"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1145\/1055686.1055690"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2422085.2422088","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2422085.2422088","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:35Z","timestamp":1750234715000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2422085.2422088"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,2]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["10.1145\/2422085.2422088"],"URL":"https:\/\/doi.org\/10.1145\/2422085.2422088","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2013,2]]},"assertion":[{"value":"2011-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}