{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:41:58Z","timestamp":1750308118537,"version":"3.41.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006,1]]},"abstract":"<jats:p>\n            The answer-set programming (ASP) paradigm is a way of using logic to solve search problems. Given a search problem, to solve it one designs a logic theory so that\n            <jats:italic>models<\/jats:italic>\n            of this theory represent problem solutions. To compute a solution to the problem, one computes a model of the theory. Several answer-set programming formalisms have been developed on the basis of logic programming with the semantics of answer sets. In this article we show that predicate logic also gives rise to effective implementations of the ASP paradigm, similar in spirit to logic programming with the answer-set semantics and with a similar scope of applicability. Specifically, we propose two logics based on predicate calculus as formalisms for encoding search problems. We show that the expressive power of these logics is given by the class NPMV. We demonstrate their use in programming and discuss computational approaches to model finding. To address this latter issue, we follow a two-pronged approach. On the one hand, we show that the problem can be reduced to that of computing models of propositional theories and, more generally, of collections of\n            <jats:italic>pseudo-Boolean<\/jats:italic>\n            constraints. Consequently, programs (solvers) developed in the areas of propositional and pseudo-Boolean satisfiability can be used to compute models of theories in our logics. On the other hand, we develop native solvers designed specifically to exploit features of our formalisms. We present experimental results demonstrating the computational effectiveness of the overall approach.\n          <\/jats:p>","DOI":"10.1145\/1119439.1119441","type":"journal-article","created":{"date-parts":[[2006,5,8]],"date-time":"2006-05-08T16:09:20Z","timestamp":1147104560000},"page":"38-83","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Predicate-calculus-based logics for modeling and solving search problems"],"prefix":"10.1145","volume":"7","author":[{"given":"Deborah","family":"East","sequence":"first","affiliation":[{"name":"Texas State University-San Marcos, San Marcos, TX"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miroslaw","family":"Truszczy\u0144ski","sequence":"additional","affiliation":[{"name":"University of Kentucky, Lexington, KY"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2006,1]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(91)90032-Z"},{"volume-title":"Proceedings of the 5th International Symposium on Theory and Applications of Satisfiability. 346--353","author":"Aloul F.","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","unstructured":"Aloul F. Ramani A. Markov I. and Sakallah K. 2003. PBS v0.2 incremental pseudo-Boolean backtrack search SAT solver and optimizer. Go online to http:\/\/www.eecs.umich.edu\/~faloul\/Tools\/pbs\/.]]  Aloul F. Ramani A. Markov I. and Sakallah K. 2003. PBS v0.2 incremental pseudo-Boolean backtrack search SAT solver and optimizer. Go online to http:\/\/www.eecs.umich.edu\/~faloul\/Tools\/pbs\/.]]"},{"volume-title":"Handbook of Theoretical Computer Science","author":"Apt K.","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","unstructured":"Babovich Y. and Lifschitz V. 2002. Cmodels Package. Go online to http:\/\/www.cs.utexas.edu\/users\/tag\/cmodels.html.]]  Babovich Y. and Lifschitz V. 2002. Cmodels Package. Go online to http:\/\/www.cs.utexas.edu\/users\/tag\/cmodels.html.]]"},{"volume-title":"Reasoning and Declarative Problem Solving","author":"Baral C.","key":"e_1_2_1_6_1"},{"volume-title":"A Davis-Putnam based elimination algorithm for linear pseudo-Boolean optimization. Tech. rep. MPI-I-95-2-003","author":"Barth P.","key":"e_1_2_1_7_1"},{"volume-title":"Proceedings of the 14th National Conference on Artificial Intelligence (AAAI-1997)","author":"Bayardo Jr., R.","key":"e_1_2_1_8_1"},{"volume":"775","volume-title":"Proceedings of the 11th Annual Symposium on Theoretical Aspects of Computer Science (STACS-1994)","author":"Benhamou B.","key":"e_1_2_1_9_1"},{"volume":"2309","volume-title":"Proceeding of the 4th International Workshop on Frontiers of Combining Systems (FroCoS-2002)","author":"Cadoli M.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00108-4"},{"volume":"2028","volume-title":"Proceedings of the European Symposium On Programming (ESOP-2001)","author":"Cadoli M.","key":"e_1_2_1_12_1"},{"volume-title":"Negation as failure","author":"Clark K.","key":"e_1_2_1_13_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"e_1_2_1_14_1","unstructured":"Colmerauer A. Kanoui H. Pasero R. and Roussel P. 1973. Un systeme de communication homme-machine en francais. Tech. rep. University of Marseille Marseille France.]]  Colmerauer A. Kanoui H. Pasero R. and Roussel P. 1973. Un systeme de communication homme-machine en francais. Tech. rep. University of Marseille Marseille France.]]"},{"volume-title":"Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI-2003)","author":"Dell'Armi T.","key":"e_1_2_1_15_1"},{"volume":"2401","volume-title":"Proceedings of the 18th International Conference on Logic Programming. Lecture Notes in Computer Science","author":"Dimopoulos Y.","key":"e_1_2_1_16_1"},{"volume-title":"The 18th National Conference on Artificial Intelligence (AAAI-2002)","author":"Dixon H.","key":"e_1_2_1_17_1"},{"volume-title":"Proccedings of the 17th National Conference on Artificial Intelligence (AAAI-2000)","author":"East D.","key":"e_1_2_1_18_1"},{"key":"e_1_2_1_19_1","unstructured":"East D. and Truszczy\u0144ski M. 2001a. ASP solver aspps. Go online to http:\/\/www.cs.uky.edu\/aspps\/.]]  East D. and Truszczy\u0144ski M. 2001a. ASP solver aspps. Go online to http:\/\/www.cs.uky.edu\/aspps\/.]]"},{"volume":"2174","volume-title":"Proceedings of Joint German\/Austrian Conference on Artificial Intelligence (KI-2001)","author":"East D.","key":"e_1_2_1_20_1"},{"volume-title":"Proceeding of the 6th International Conference on Knowledge Representation and Reasoning (KR-1998)","author":"Eiter T.","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068403001765"},{"volume-title":"Complexity of Computation","author":"Fagin R.","key":"e_1_2_1_23_1"},{"volume-title":"AMPL: A Modeling Language for Mathematical Programming","year":"1993","author":"Fourer R.","key":"e_1_2_1_24_1"},{"volume-title":"Proceedings of the 5th International Conference on Logic Programming. MIT Press","author":"Gelfond M.","key":"e_1_2_1_25_1"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037169"},{"volume-title":"Proceedings of the 7th International Conference on Principles of Knowledge Representation and Reasoning, (KR-2000)","author":"Ginsberg M.","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/795666.796598"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA459656"},{"volume-title":"Proceedings of 5th International Conference on Principles of Knowledge Representation and Reasoning (KR-1996)","author":"Kautz H.","key":"e_1_2_1_30_1"},{"volume-title":"Proceedings of the Congress of the International Federation for Information Processing (IFIP-1974)","year":"1974","author":"Kowalski R.","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","unstructured":"Leone N. Pfeifer G. Faber W. Eiter T. Gottlob G. Perri S. and Scarcello F. 2003. The dlv system for knowledge representation and reasoning. Go online to http:\/\/xxx.lanl.gov\/abs\/cs.AI\/0211004.]]  Leone N. Pfeifer G. Faber W. Eiter T. Gottlob G. Perri S. and Scarcello F. 2003. The dlv system for knowledge representation and reasoning. Go online to http:\/\/xxx.lanl.gov\/abs\/cs.AI\/0211004.]]"},{"key":"e_1_2_1_33_1","unstructured":"Li C. 1997. SAT solver satz. Go online to http:\/\/www.laria.u-picardie.fr\/~cli\/EnglishPage.html.]]  Li C. 1997. SAT solver satz. Go online to http:\/\/www.laria.u-picardie.fr\/~cli\/EnglishPage.html.]]"},{"volume":"1330","volume-title":"Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming. Lecture Notes in Computer Science","author":"Li C.","key":"e_1_2_1_34_1"},{"volume-title":"ASSAT: Computing answer sets of a logic program by SAT solvers. In Proccedings of the 18th National Conference on Artificial Intelligence (AAAI-2002)","year":"2002","author":"Lin F.","key":"e_1_2_1_35_1"},{"volume":"2833","volume-title":"Proceedings of the 9th International Conference on Principles and Practice of Constraint Programming, CP-2003","author":"Liu L.","key":"e_1_2_1_36_1"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068403001777"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Marek V. and Truszczy\u0144ski M. 1999. Stable models and an alternative logic programming paradigm. In The Logic Programming Paradigm: A 25-Year Perspective K. Apt W. Marek M. Truszczy\u0144ski and D. Warren Eds. Springer Berlin Germany 375--398.]]  Marek V. and Truszczy\u0144ski M. 1999. Stable models and an alternative logic programming paradigm. In The Logic Programming Paradigm: A 25-Year Perspective K. Apt W. Marek M. Truszczy\u0144ski and D. Warren Eds. Springer Berlin Germany 375--398.]]","DOI":"10.1007\/978-3-642-60085-2_17"},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Marek W. and Truszczy\u0144ski M. 1993. Nonmonotonic Logic; Context-Dependent Reasoning. Springer Berlin Germany.]]   Marek W. and Truszczy\u0144ski M. 1993. Nonmonotonic Logic; Context-Dependent Reasoning. Springer Berlin Germany.]]","DOI":"10.1007\/978-3-662-02906-0"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(80)90009-0"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Moskewicz M. Madigan C. Zhao Y. Zhang L. and Malik S. 2001b. SAT solver chaff. Go online to http:\/\/www.ee.princeton.edu\/~chaff\/.]]  Moskewicz M. Madigan C. Zhao Y. Zhang L. and Malik S. 2001b. SAT solver chaff. Go online to http:\/\/www.ee.princeton.edu\/~chaff\/.]]","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_43_1","unstructured":"Nerode A. and Shore R. 1993. Logic and Logic Programming. Springer Berlin Germany.]]   Nerode A. and Shore R. 1993. Logic and Logic Programming. Springer Berlin Germany.]]"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018930122475"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Niemel\u00e4 I. and Simons P. 2000. Extending the smodels system with cardinality and weight constraints. In Logic-Based Artificial Intelligence J. Minker Ed. Kluwer Academic Publishers Dordrecht The Netherlands 491--521.]]   Niemel\u00e4 I. and Simons P. 2000. Extending the smodels system with cardinality and weight constraints. In Logic-Based Artificial Intelligence J. Minker Ed. Kluwer Academic Publishers Dordrecht The Netherlands 491--521.]]","DOI":"10.1007\/978-1-4615-1567-8_21"},{"key":"e_1_2_1_46_1","unstructured":"Niemel\u00e4 I. Simons P. and Syrj\u00e4nen T. 1997. SLP solver smodels. Go online to http:\/\/www.tcs.hut.fi\/Software\/smodels\/.]]  Niemel\u00e4 I. Simons P. and Syrj\u00e4nen T. 1997. SLP solver smodels. Go online to http:\/\/www.tcs.hut.fi\/Software\/smodels\/.]]"},{"volume-title":"Proceedings of the 4th International Workshop on Integration of AI and OR techniques in Constraint Programming for Combinatorial Optimisation Problems, (CPAIOR-2002)","year":"2002","author":"Prestwich S.","key":"e_1_2_1_48_1"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1997.1446"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1995.1053"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(05)80009-1"},{"volume-title":"Proceedings of the 12th National Conference on Artificial Intelligence (AAAI-1994)","author":"Selman B.","key":"e_1_2_1_53_1"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00187-X"},{"volume-title":"Principles of Database and Knowledge-Base Systems","author":"Ullman J.","key":"e_1_2_1_55_1"},{"volume-title":"The OPL Optimization Programming Language","author":"van Hentenryck P.","key":"e_1_2_1_56_1"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802186"},{"volume-title":"Eclipse: A platform for constraint logic programming. Go online to http:\/\/www.icparc.ic.ac.uk\/eclipse\/reports\/eclipse.ps.gz.]]","year":"1997","author":"Wallace M.","key":"e_1_2_1_58_1"},{"volume-title":"Proceedings of the 11th National Conference on Artificial Intelligence (AAAI-97)","year":"1997","author":"Walser J.","key":"e_1_2_1_59_1"},{"volume-title":"Challenges in SAT (and QBF). Invited talk at 6th International Conference on Theory and Applications of Satisfiability Testing. Slides available online from http:\/\/4c.ucc.ie\/tw\/sat2003.ppt.]]","author":"Walsh T.","key":"e_1_2_1_60_1"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1119439.1119441","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1119439.1119441","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:18Z","timestamp":1750262898000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1119439.1119441"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1]]},"references-count":59,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,1]]}},"alternative-id":["10.1145\/1119439.1119441"],"URL":"https:\/\/doi.org\/10.1145\/1119439.1119441","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2006,1]]},"assertion":[{"value":"2006-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}