{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T01:23:49Z","timestamp":1773278629246,"version":"3.50.1"},"reference-count":65,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2006,9,29]],"date-time":"2006-09-29T00:00:00Z","timestamp":1159488000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,1,2]]},"DOI":"10.1007\/s10817-006-9033-2","type":"journal-article","created":{"date-parts":[[2006,9,28]],"date-time":"2006-09-28T09:47:17Z","timestamp":1159436837000},"page":"345-377","source":"Crossref","is-referenced-by-count":94,"title":["Answer Set Programming Based on Propositional Satisfiability"],"prefix":"10.1007","volume":"36","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuliya","family":"Lierler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Maratea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,9,29]]},"reference":[{"key":"9033_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Lecture Notes in Computer Science, vol. 1809, pp. 97\u2013108 (1999)","DOI":"10.1007\/10720246_8"},{"key":"9033_CR2","doi-asserted-by":"crossref","unstructured":"Armando, A., Castellini, C., Giunchiglia, E., Maratea, M.: The SAT-based approach to separation logic. J. Autom. Reason. To appear (2005)","DOI":"10.1007\/s10817-005-9002-1"},{"key":"9033_CR3","unstructured":"Babovich, Y., Erdem, E., Lifschitz, V.: \u2018Fages\u2019 theorem and answer set programming. In: Proc. NMR, (2000)"},{"key":"9033_CR4","unstructured":"Baral, C., Gelfond, M., Scherl, R.: \u2018Using answer set programming to answer complex queries. In: Workshop on Pragmatics of Question Answering at HLT-NAAC2004, (2004)"},{"key":"9033_CR5","first-page":"236","volume-title":"14th International Conference on Computer Aided Verification (CAV), vol. 2404 of Lecture Notes in Computer Science","author":"C.W. Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental Translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.), 14th International Conference on Computer Aided Verification (CAV), vol. 2404 of Lecture Notes in Computer Science, pp. 236\u2013249. Springer, Berlin Heidelberg New York (2002)"},{"key":"9033_CR6","unstructured":"Bayardo, R.J. Jr, Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI-97\/IAAI-97). Menlo Park, California, pp. 203\u2013208. AAAI (1997)"},{"key":"9033_CR7","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/BF01530761","volume":"12","author":"R. Ben-Eliyahu","year":"1996","unstructured":"Ben-Eliyahu, R., Dechter, R.: Propositional semantics for disjunctive logic programs. Ann. Math. Artif. Intell. 12, 53\u201387 (1996)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9033_CR8","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-1-4684-3384-5_11","volume-title":"Logic and Data Bases","author":"K. Clark","year":"1978","unstructured":"Clark, K.: Negation as failure. In: Gallaire, H., Minker, J. (eds.), Logic and Data Bases, pp. 293\u2013322. Plenum, New York (1978)"},{"key":"9033_CR9","doi-asserted-by":"crossref","unstructured":"\u015etef\u0103nescu, A., Esparza, J., Muscholl, A.: Synthesis of distributed algorithms using asynchronous automata. In: Proc. CONCUR'03, vol. 2761, pp. 27\u201341. Springer (2003)","DOI":"10.1007\/978-3-540-45187-7_2"},{"issue":"7","key":"9033_CR10","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"9033_CR11","doi-asserted-by":"crossref","unstructured":"de Moura, L., Rue\u00df, H., Sorea, S.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.), Automated Deduction \u2013 CADE-18, vol. 2392 of Lecture Notes in Computer Science, pp. 438\u2013455. Springer (2002)","DOI":"10.1007\/3-540-45620-1_35"},{"key":"9033_CR12","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1613\/jair.1555","volume":"22","author":"H.E. Dixon","year":"2004","unstructured":"Dixon, H.E., Ginsberg, M.L., Luks, E.M., Parkes, A.J.: Generalizing Boolean satisfiability II: Theory. J. Artif. Intell. Res. (JAIR) 22, 481\u2013534 (2004)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"9033_CR13","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"3","author":"W. Dowling","year":"1984","unstructured":"Dowling, W., Gallier, J.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 3, 267\u2013284 (1984)","journal-title":"J. Log. Program."},{"key":"9033_CR14","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver'. In: Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5\u20138, 2003 Selected Revised Papers, pp. 502\u2013518, (2003)"},{"key":"9033_CR15","unstructured":"Erdem, E.: Theory and applications of answer set programming. Ph.D. thesis, University of Texas at Austin (2002)"},{"key":"9033_CR16","doi-asserted-by":"crossref","unstructured":"Erdem, E., Lifschitz, V.: \u2018Fages\u2019 theorem for programs with nested expressions. In: Proc. International Conference on Logic Programming, pp. 242\u2013254, (2001)","DOI":"10.1007\/3-540-45635-X_24"},{"key":"9033_CR17","unstructured":"Faber, W., Leone, N., Pfeifer, G.: Experimenting with heuristics for answer set programming. In: IJCAI, pp. 635\u2013640 (2001)"},{"key":"9033_CR18","first-page":"51","volume":"1","author":"F. Fages","year":"1994","unstructured":"Fages, F.: Consistency of Clark's completion and existence of stable models. J. Methods Logic Comput. Sci. 1, 51\u201360 (1994)","journal-title":"J. Methods Logic Comput. Sci."},{"key":"9033_CR19","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1017\/S1471068403001923","volume":"5","author":"P. Ferraris","year":"2005","unstructured":"Ferraris, P., Lifschitz, V.: Weight constraints as nested expressions. Theory and Practice of Logic Programming 5, 45\u201374 (2005)","journal-title":"Theory and Practice of Logic Programming"},{"key":"9033_CR20","doi-asserted-by":"crossref","unstructured":"Gebser, M., Schaub, T.: Loops: Relevant or redundant?. In: Proceedings of 8th International Conference on Logic Programming and Nonmonotonic Reasoning, pp. 53\u201365. Springer (2005)","DOI":"10.1007\/11546207_5"},{"key":"9033_CR21","unstructured":"Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R., Bowen, K. (eds.) Logic Programming: Proceedings of the Fifth Int'l Conf. and Symp., pp. 1070\u20131080, (1988)"},{"key":"9033_CR22","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/BF03037169","volume":"9","author":"M. Gelfond","year":"1991","unstructured":"Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases. New Gener. Comput. 9, 365\u2013385 (1991)","journal-title":"New Gener. Comput."},{"key":"9033_CR23","unstructured":"Gent, I., Maaren, H.V., Walsh, T. (eds.) SAT 2000. Highlights of Satisfiability Research in the Year 2000. IOS (2000)"},{"key":"9033_CR24","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1023\/A:1015071400913","volume":"28","author":"E. Giunchiglia","year":"2002","unstructured":"Giunchiglia, E., Giunchiglia, F., Tacchella, A.: SAT-based decision procedures for classical modal logics. J. Autom. Reason. 28, 143\u2013171 (2002). Reprinted in [23]","journal-title":"J. Autom. Reason."},{"key":"9033_CR25","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Maratea, M.: On the relation between SAT and ASP procedures (or, between smodels and cmodels). In: Proceedings of the 21th International Conference on Logic Programming (ICLP), pp. 37\u201351. Springer (2005a)","DOI":"10.1007\/11562931_6"},{"key":"9033_CR26","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Maratea, M.: Evaluating search strategies and heuristics for efficient answer set programming. In: Advanced in Artificial Intelligence: Conference of the Italian Association for Artificial Intelligence, AI*IA '05, Milan, Italy, September 20\u201323, 2005, Proceedings, pp. 37\u201351. Springer (2005b)","DOI":"10.1007\/11558590_13"},{"key":"9033_CR27","unstructured":"Giunchiglia, E., Maratea, M., Lierler, Y.: SAT-based answer set programming. In: Proc. 19th National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, July 25-29, 2004, San Jose, California. AAAI, The MIT Press (2004)"},{"key":"9033_CR28","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Maratea, M., Tacchella, A.: In: Effectiveness of look-ahead techniques in a modern SAT solver. In: 9th International Conference on Principles and Practice of Constraint Programming (CP-03), pp. 842\u2013846, (2003)","DOI":"10.1007\/978-3-540-45193-8_64"},{"key":"9033_CR29","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Maratea, M., Tacchella, A., Zambonin, D.: Evaluating search heuristics and optimization techniques in propositional satisfiability. In: Automated Reasoning, First International Joint Conference (IJCAR), vol. 2083 of Lecture Notes in Computer Science, pp. 347\u2013363. Springer (2001)","DOI":"10.1007\/3-540-45744-5_26"},{"key":"9033_CR30","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT solver. In: Proc. of the Design, Automation and Test in Europe Conference and Exposition 2003, pp. 142\u2013149. IEEE Computer Society (2003)","DOI":"10.1109\/DATE.2002.998262"},{"issue":"4&5","key":"9033_CR31","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1017\/S1471068403001790","volume":"3","author":"K. Heljanko","year":"2003","unstructured":"Heljanko, K., Niemel\u00e4, I.: Bounded LTL model checking with stable models. Theory and Practice of Logic Programming 3(4&5), 519\u2013550 (2003). Also available as (CoRR: arXiv:cs.LO\/0305040)","journal-title":"Theory and Practice of Logic Programming"},{"key":"9033_CR32","unstructured":"Janhunen, T.: Translatability and intranslatability results for certain classes of logic programs'. Series A: Research report 82, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland (2003)"},{"key":"9033_CR33","unstructured":"Janhunen, T.: Representing normal programs with clauses. In: Proc. of 16th European Conference on Artificial Intelligence, ECAI 2004, pp. 358\u2013362. IOS (2004)"},{"key":"9033_CR34","doi-asserted-by":"crossref","unstructured":"Janhunen, T., Niemel\u00e4, I.: GnT \u2013 A solver for disjunctive logic programming. In: Proc. of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), pp. 331\u2013335. Springer (2004)","DOI":"10.1007\/978-3-540-24609-1_29"},{"key":"9033_CR35","doi-asserted-by":"crossref","unstructured":"Janhunen, T., Niemel\u00e4, I., Seipel, D., Simons, P., You, J.-H.: Unfolding partiality and disjuntion in stable model semantics. Accepted to the ACM Transaction on Computational Logic (2005)","DOI":"10.1145\/1119439.1119440"},{"key":"9033_CR36","unstructured":"Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, Oregon, November 6\u20138, 2002, Proceedings, pp. 142\u2013159 (2002)"},{"key":"9033_CR37","unstructured":"Le Berre, D., Simon, L.: The essentials of the SAT'03 Competition'. In: Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5\u20138, 2003 Selected Revised Papers, vol. 2919 of LNCS (2003)"},{"key":"9033_CR38","doi-asserted-by":"crossref","unstructured":"Lee, J., Lifschitz, V.: Loop formulas for disjunctive logic programs. In: Proc. ICLP-03, (2003)","DOI":"10.1007\/978-3-540-24599-5_31"},{"key":"9033_CR39","doi-asserted-by":"crossref","unstructured":"Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., Scarcello, F.: The DLV system for knowledge representation and reasoning. Accepted to ACM Transactions on Computational Logic (ToCL) (2005)","DOI":"10.1145\/1149114.1149117"},{"key":"9033_CR40","unstructured":"Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97). San Francisco, pp. 366\u2013371, Morgan Kaufmann (1997)"},{"key":"9033_CR41","unstructured":"Lierler, Y.: Disjunctive answer set programming via satisfiability. In: Answer Set Programming, vol. 142 of CEUR Workshop Proceedings (2005)"},{"key":"9033_CR42","unstructured":"Lierler, Y., Lifschitz, V.: Computing answer sets using program completion. Available at http:\/\/www.cs.utexas.edu\/users\/tag\/cmodels.html , 2003"},{"key":"9033_CR43","unstructured":"Lifschitz, V.: Foundations of logic programming. In: Brewka, G. (ed.), Principles of Knowledge Representation. CSLI, pp. 69\u2013128, (1996)"},{"key":"9033_CR44","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1145\/1131313.1131316","volume":"7","author":"V. Lifschitz","year":"2006","unstructured":"Lifschitz, V., Razborov, A.: Why are there so many loop formulas? ACM Transactions on Computational Logic, 7, 261\u2013268 (2006)","journal-title":"ACM Transactions on Computational Logic"},{"key":"9033_CR45","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1023\/A:1018978005636","volume":"25","author":"V. Lifschitz","year":"1999","unstructured":"Lifschitz, V., Tang, L.R., Turner, H.: Nested expressions in logic programs. Ann. Math. Artif. Intell. 25, 369\u2013389 (1999)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9033_CR46","unstructured":"Lin, F., Zhao, J.: On tight logic programs and yet another translation from normal logic programs to propositional logic. In: Proc. IJCAI (2003a)"},{"key":"9033_CR47","unstructured":"Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by SAT Solvers. In: Proc. 18th National Conference on Artificial Intelligence and Fourteenth Conference on Innovative Applications of Artificial Intelligence (AAAI\/IAAI-02). Menlo Park, California, pp. 112\u2013118. AAAI (2002)"},{"key":"9033_CR48","doi-asserted-by":"crossref","unstructured":"Lin, F., Zhao, Y.: Answer set programming phase transition: A study on randomly generated programs. In: Proc. ICLP, (2003b)","DOI":"10.1007\/978-3-540-24599-5_17"},{"issue":"1\u20132","key":"9033_CR49","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/j.artint.2004.04.004","volume":"157","author":"F. Lin","year":"2004","unstructured":"Lin, F., Zhao, Y.: ASSAT: computing answer sets of a logic program by SAT solvers. Artif. Intell. 157(1\u20132), 115\u2013137 (2004)","journal-title":"Artif. Intell."},{"key":"9033_CR50","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0743-1066(84)90011-6","volume":"3","author":"J. Lloyd","year":"1984","unstructured":"Lloyd, J., Topor, R.: Making Prolog more expressive. J. Log. Program. 3, 225\u2013240 (1984)","journal-title":"J. Log. Program."},{"key":"9033_CR51","unstructured":"Marek, V., Subrahmanian, V.: The relationship between logic program semantics and non-monotonic reasoning. In: Levi, G., Martelli, M. (eds.) Logic Programming: Proceedings of the 6th Int'l Conf., pp. 600\u2013617, (1989)"},{"key":"9033_CR52","doi-asserted-by":"crossref","unstructured":"Marek, V., Truszczynski, M.: Stable models as an alternative programming paradigm. In: The Logic Programming Paradigm: A 25 Years perspective, Lecture Notes in Computer Science. Springer (1999)","DOI":"10.1007\/978-3-642-60085-2_17"},{"key":"9033_CR53","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. 38th Design Automation Conference (DAC'01), pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"9033_CR54","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1023\/A:1018930122475","volume":"25","author":"I. Niemel\u00e4","year":"1999","unstructured":"Niemel\u00e4, I.: Logic programs with stable model semantics as a constraint programming paradigm. Ann. Math. Artif. Intell. 25, 241\u2013273 (1999)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9033_CR55","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6\u201310, 2005, Proceedings, pp. 321\u2013334, (2005)"},{"key":"9033_CR56","doi-asserted-by":"crossref","unstructured":"Nogueira, M., Balduccini, M., Gelfond, M., Watson, R., Barry, M.: An A-Prolog decision support system for the space shuttle. In: Working Notes of the AAAI Spring Symposium on Answer Set Programming, (2001)","DOI":"10.1007\/3-540-45241-9_12"},{"key":"9033_CR57","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. Plaisted","year":"1986","unstructured":"Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symbol. Comput. 2, 293\u2013304 (1986)","journal-title":"J. Symbol. Comput."},{"key":"9033_CR58","unstructured":"Sheridan, D.: The Optimality of a Fast CNF Conversion and its use with SAT. In: Proceedings of SAT, International Conference on Theory and Applications of Satisfiability Testing, Vancouver (Canada) (2004)"},{"key":"9033_CR59","doi-asserted-by":"crossref","unstructured":"Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970, Vol. 1\u20132. Springer (1983)","DOI":"10.1007\/978-3-642-81952-0"},{"key":"9033_CR60","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP \u2013 A New Search Algorithm for Satisfiability. Technical report, University of Michigan, (1996)"},{"issue":"1\u20132","key":"9033_CR61","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/S0004-3702(02)00187-X","volume":"138","author":"P. Simons","year":"2002","unstructured":"Simons, P., Niemel\u00e4, I., Timo, S.: Extending and implementing the stable model semantics. Artif. Intell. 138(1\u20132), 181\u2013234 (2002)","journal-title":"Artif. Intell."},{"key":"9033_CR62","unstructured":"Syrjanen, T.: Lparse Manual. http:\/\/www.tcs.hut.fi\/Software\/smodels\/lparse.ps.gz , 2003"},{"key":"9033_CR63","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of proofs in propositional logics. Semin. Math. 8 (1970). Reprinted in [59].","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"9033_CR64","unstructured":"Ward, J., Schlipf, J.S.: Answer set programming with clause learning. In: Logic Programming and Nonmonotonic Reasoning, 7th International Conference, LPNMR 2004, Fort Lauderdale, Florida, January 6\u20138, 2004, Proceedings, pp. 302\u2013313 (2004)"},{"key":"9033_CR65","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: International Conference on Computer-Aided Design (ICCAD'01), pp. 279\u2013285, (2001)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9033-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9033-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9033-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T01:30:58Z","timestamp":1736559058000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9033-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,9,29]]},"references-count":65,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2007,1,2]]}},"alternative-id":["9033"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9033-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,9,29]]}}}