{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T12:35:59Z","timestamp":1763642159138,"version":"3.37.3"},"reference-count":81,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,12,16]],"date-time":"2016-12-16T00:00:00Z","timestamp":1481846400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2017,7]]},"DOI":"10.1007\/s10601-016-9257-7","type":"journal-article","created":{"date-parts":[[2016,12,17]],"date-time":"2016-12-17T05:38:17Z","timestamp":1481953097000},"page":"307-337","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["What is answer set programming to propositional satisfiability"],"prefix":"10.1007","volume":"22","author":[{"given":"Yuliya","family":"Lierler","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,12,16]]},"reference":[{"key":"9257_CR1","doi-asserted-by":"crossref","unstructured":"Alviano, M., Dodaro, C., Faber, W., Leone, N., & Ricca, F. (2013). WASP: a native ASP solver based on constraint learning. In Proc. of LPNMR 2013. Vol. 8148 of LNCS (pp. 54\u201366). Springer-Verlag.","DOI":"10.1007\/978-3-642-40564-8_6"},{"key":"9257_CR2","doi-asserted-by":"crossref","unstructured":"Alviano, M., Dodaro, C., Faber, W., Leone, N., & Ricca, F. (2015). Advances in WASP. In Proc. of LPNMR 2015. Vol. 9345 of LNCS (pp. 40\u201354). Springer-Verlag.","DOI":"10.1007\/978-3-319-23264-5_5"},{"key":"9257_CR3","unstructured":"Anger, C., Gebser, M., Janhunen, T., & Schaub, T. (2006). What\u2019s a head without a body? In Proceedings of the European conference on artificial intelligence (ECAI\u201906) (pp. 769\u2013770)."},{"key":"9257_CR4","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1613\/jair.3152","volume":"40","author":"A Atserias","year":"2011","unstructured":"Atserias, A., Fichte, J. K., & Thurley, M. (2011). Clause-learning algorithms with many restarts and bounded-width resolution. Journal of Artificial Inteligence Research (JAIR), 40, 353\u2013373.","journal-title":"Journal of Artificial Inteligence Research (JAIR)"},{"key":"9257_CR5","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E. M., Strichman, O., & Zhu, Y. (2003). Bounded model checking. Advances in Computers, 58, 117\u2013148.","journal-title":"Advances in Computers"},{"key":"9257_CR6","unstructured":"Biere, A., Heule, M., van Maaren, H., & Walsh, T. (2009). Handbook of satisfiability: volume 185 frontiers in artificial intelligence and applications. Amsterdam: IOS Press."},{"issue":"12","key":"9257_CR7","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1145\/2043174.2043195","volume":"54","author":"G Brewka","year":"2011","unstructured":"Brewka, G., Eiter, T., & Truszczy\u0144ski, M. (2011). Answer set programming at a glance. Communications of the ACM, 54(12), 92\u2013103.","journal-title":"Communications of the ACM"},{"key":"9257_CR8","doi-asserted-by":"crossref","first-page":"854","DOI":"10.1017\/S1471068414000623","volume":"15","author":"M Calautti","year":"2015","unstructured":"Calautti, M., Greco, S., Spezzano, F., & Trubitsyna, I. (2015). Checking termination of bottom-up evaluation of logic programs with function symbols. Theory and Practice of Logic Programming, 15, 854\u2013889. http:\/\/journals.cambridge.org\/article_S1471068414000623 .","journal-title":"Theory and Practice of Logic Programming"},{"key":"9257_CR9","doi-asserted-by":"crossref","unstructured":"Calimeri, F., Cozza, S., Ianni, G., & Leone, N. (2008). Computable functions in ASP: theory and implementation. In Proceedings of international conference on logic programming (ICLP) (pp. 407\u2013424).","DOI":"10.1007\/978-3-540-89982-2_37"},{"key":"9257_CR10","doi-asserted-by":"crossref","unstructured":"Clark, K. (1978). Negation as failure. In Gallaire, H., & Minker, J (Eds.) Logic and data bases (pp. 293\u2013322). New York: Plenum Press.","DOI":"10.1007\/978-1-4684-3384-5_11"},{"issue":"7","key":"9257_CR11","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. (1962). A machine program for theorem proving. Communications of the ACM, 5(7), 394\u2013397.","journal-title":"Communications of the ACM"},{"key":"9257_CR12","doi-asserted-by":"crossref","unstructured":"Denecker, M. (2000). Extending classical logic with inductive definitions. In LNAI (pp. 703\u2013717). Springer-Verlag.","DOI":"10.1007\/3-540-44957-4_47"},{"key":"9257_CR13","unstructured":"Denecker, M., Lierler, Y., Truszczy\u0144ski, M., & Vennekens, J. (2012). A tarskian informal semantics for answer set programming. In Technical communications of the 28th international conference on logic programming (ICLP) (pp. 277\u2013289)."},{"issue":"1","key":"9257_CR14","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1145\/1119439.1119441","volume":"7","author":"D East","year":"2006","unstructured":"East, D., & Truszczy\u0144ski, M. (2006). Predicate-calculus-based logics for modeling and solving search problems. ACM Transactions on Computing Logic, 7(1), 38\u201383.","journal-title":"ACM Transactions on Computing Logic"},{"key":"9257_CR15","unstructured":"Een, N., & Biere, A. (2005). Effective preprocessing in SAT through variable and clause elimination. In SAT."},{"key":"9257_CR16","unstructured":"Eiter, T., & Gottlob, G. (1993). Complexity results for disjunctive logic programming and application to nonmonotonic logics. In Miller, D (Ed.) Proceedings of international logic programming symposium (ILPS) (pp. 266\u2013278)."},{"key":"9257_CR17","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/BF03037172","volume":"9","author":"F Fages","year":"1991","unstructured":"Fages, F. (1991). A fixpoint semantics for general logic programs compared with the well-supported and stable model semantics. New Generation Computing, 9, 425\u2013443.","journal-title":"New Generation Computing"},{"key":"9257_CR18","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1017\/S1471068403001923","volume":"5","author":"P Ferraris","year":"2005","unstructured":"Ferraris, P., & Lifschitz, V. (2005). Weight constraints as nested expressions. Theory and Practice of Logic Programming, 5, 45\u201374.","journal-title":"Theory and Practice of Logic Programming"},{"key":"9257_CR19","unstructured":"Gebser, M., Guziolowski, C., Ivanchev, M., Schaub, T., Siegel, A., Thiele, S., & Veber, P. (2010). Repair and prediction (under inconsistency) in large biological networks with answer set programming. In Lin, F., Sattler, U., & Truszczynski, M (Eds.) Proceedings of the 12th international conference on principles of knowledge representation and reasoning KR 2010: AAAI Press."},{"key":"9257_CR20","unstructured":"Gebser, M., Harrison, A., Kaminski, R., Lifschitz, V., & Schaub, T. (2015). Abstract gringo, (Vol. 15. http:\/\/journals.cambridge.org\/article_S1471068415000150 ."},{"key":"9257_CR21","unstructured":"Gebser, M., Janhunen, T., Kaminski, R., Schaub, T., & Tasharrofi, S. (2015). Writing declarative specifications for clauses. In Proceedings of the 3rd workshop on grounding, transforming, and modularizing theories with variables."},{"key":"9257_CR22","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Lindauer, M., Ostrowski, M., Romero, J., Schaub, T., & Thiele, S. (2015). Potassco user guide., available at https:\/\/sourceforge.net\/projects\/potassco\/files\/guide\/2.0\/guide-2.0.pdf ."},{"key":"9257_CR23","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., & Thiele, S. (2010). A user\u2019s guide to gringo, clasp, clingo, and iclingo., available at http:\/\/potassco.sourceforge.net ."},{"key":"9257_CR24","first-page":"250","volume-title":"On the implementation of weight constraint rules in conflict-driven ASP solvers","author":"M Gebser","year":"2009","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., & Schaub, T. (2009). On the implementation of weight constraint rules in conflict-driven ASP solvers, (pp. 250\u2013264). Berlin, Heidelberg: Springer Berlin Heidelberg."},{"key":"9257_CR25","doi-asserted-by":"crossref","unstructured":"Gebser, M., Kaminski, R., & Schaub, T. (2011). aspcud: a linux package configuration tool based on answer set programming. In Second international workshop on logics for component configuration (LoCoCo).","DOI":"10.4204\/EPTCS.65.2"},{"key":"9257_CR26","unstructured":"Gebser, M., Kaufmann, B., Neumann, A., & Schaub, T. (2007). Conflict-driven answer set solving. In Proceedings of 20th international joint conference on artificial intelligence (IJCAI\u201907) (pp. 386\u2013392). MIT Press."},{"key":"9257_CR27","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1016\/j.artint.2012.04.001","volume":"187","author":"M Gebser","year":"2012","unstructured":"Gebser, M., Kaufmann, B., & Schaub, T. (2012). Conflict-driven answer set solving: from theory to practice. Artificial Intelligence, 187, 52\u201389.","journal-title":"Artificial Intelligence"},{"key":"9257_CR28","doi-asserted-by":"crossref","unstructured":"Gebser, M., K\u00f6nig, A., Schaub, T., Thiele, S., & Veber, P. (2010). The bioASP library: ASP solutions for systems biology. In 22nd IEEE International conference on tools with artificial intelligence, ICTAI 2010 (pp. 383\u2013389). IEEE Computer Society.","DOI":"10.1109\/ICTAI.2010.62"},{"key":"9257_CR29","doi-asserted-by":"crossref","unstructured":"Gebser, M., Schaub, T., & Thiele, S. (2007). Gringo: a new grounder for answer set programming. In Proceedings of the ninth international conference on logic programming and nonmonotonic reasoning (pp. 266\u2013271).","DOI":"10.1007\/978-3-540-72200-7_24"},{"key":"9257_CR30","unstructured":"Gelfond, M., & Lifschitz, V. (1988). The stable model semantics for logic programming. In Kowalski, R., & Bowen, K (Eds.) Proceedings of international logic programming conference and symposium (pp. 1070\u20131080): MIT Press."},{"key":"9257_CR31","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/s10817-006-9033-2","volume":"36","author":"E Giunchiglia","year":"2006","unstructured":"Giunchiglia, E., Lierler, Y., & Maratea, M. (2006). Answer set programming based on propositional satisfiability. Journal of Automated Reasoning, 36, 345\u2013377.","journal-title":"Journal of Automated Reasoning"},{"key":"9257_CR32","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., & Maratea, M. (2005). On the relation between answer set and SAT procedures (or, between smodels and cmodels). In Proceedings of 21st international conference on logic programming (ICLP) (pp. 37\u201351). Springer-Verlag.","DOI":"10.1007\/11562931_6"},{"key":"9257_CR33","unstructured":"Gomes, C. P., Kautz, H., Sabharwal, A., & Selman, B. (2008). Satisfiability solvers. In van Harmelen, F., Lifschitz, V., & Porter, B (Eds.) Handbook of knowledge representation (pp. 89\u2013134): Elsevier."},{"key":"9257_CR34","unstructured":"Janhunen, T. (2004). Representing normal programs with clauses. In Proceedings of 16th European conference on artificial intelligence, ECAI 2004 (pp. 358\u2013362). IOS Press."},{"key":"9257_CR35","doi-asserted-by":"crossref","unstructured":"Janhunen, T. (2006). Some (in)translatability results for normal logic programs and propositional theories. Journal of Applied Non-Classical Logics, 35\u201386.","DOI":"10.3166\/jancl.16.35-86"},{"key":"9257_CR36","unstructured":"Kautz, H., & Selman, B. (1992). Planning as satisfiability. In Proceedings of European conference on artificial intelligence (ECAI) (pp. 359\u2013363)."},{"key":"9257_CR37","unstructured":"Lee, J. (2005). A model-theoretic counterpart of loop formulas. In Proceedings of international joint conference on artificial intelligence (IJCAI) (pp. pp. 503\u2013508). Professional Book Center."},{"issue":"3","key":"9257_CR38","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1145\/1149114.1149117","volume":"7","author":"N Leone","year":"2006","unstructured":"Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., & Scarcello, F. (2006). The dlv system for knowledge representation and reasoning. ACM Transactions on Computational Logic, 7(3), 499\u2013 562.","journal-title":"ACM Transactions on Computational Logic"},{"issue":"2","key":"9257_CR39","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1006\/inco.1997.2630","volume":"135","author":"N Leone","year":"1997","unstructured":"Leone, N., Rullo, P., & Scarcello, F. (1997). Disjunctive stable models: unfounded sets, fixpoint semantics, and computation. Information and Computation, 135(2), 69\u2013112.","journal-title":"Information and Computation"},{"key":"9257_CR40","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1017\/S1471068410000578","volume":"11","author":"Y Lierler","year":"2011","unstructured":"Lierler, Y. (2011). Abstract answer set solvers with backjumping and learning. Theory and Practice of Logic Programming, 11, 135\u2013169.","journal-title":"Theory and Practice of Logic Programming"},{"key":"9257_CR41","unstructured":"Lierler, Y., & Lifschitz, V. (2013). Logic programs vs. first-order formulas in textual inference. In 10th International conference on computational semantics (IWCS)."},{"issue":"4\u20135","key":"9257_CR42","first-page":"629","volume":"11","author":"Y Lierler","year":"2011","unstructured":"Lierler, Y., & Truszczy\u0144ski, M. (2011). Transition systems for model generators \u2014 a unifying approach. Theory and Practice of Logic Programming, 27th Int\u2019l. Conference on Logic Programming (ICLP) Special Issue, 11(4\u20135), 629\u2013646.","journal-title":"Theory and Practice of Logic Programming, 27th Int\u2019l. Conference on Logic Programming (ICLP) Special Issue"},{"key":"9257_CR43","unstructured":"Lifschitz, V. (1996). Foundations of logic programming. In Brewka, G (Ed.) Principles of knowledge representation (pp. 69\u2013128): CSLI Publications."},{"key":"9257_CR44","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/S0004-3702(02)00186-8","volume":"138","author":"V Lifschitz","year":"2002","unstructured":"Lifschitz, V. (2002). Answer set programming and plan generation. Artificial Intelligence, 138, 39\u2013 54.","journal-title":"Artificial Intelligence"},{"key":"9257_CR45","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1145\/1131313.1131316","volume":"7","author":"V Lifschitz","year":"2006","unstructured":"Lifschitz, V., & Razborov, A. (2006). Why are there so many loop formulas? ACM Transactions on Computational Logic, 7, 261\u2013268.","journal-title":"ACM Transactions on Computational Logic"},{"key":"9257_CR46","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. (1999). Nested expressions in logic programs. Annals of Mathematics and Artificial Intelligence, 25, 369\u2013389.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"9257_CR47","unstructured":"Lin, F., & Zhao, Y. (2002). ASSAT: computing answer sets of a logic program by SAT solvers. In Proceedings of national conference on artificial intelligence (AAAI) (pp. 112\u2013117). MIT Press."},{"key":"9257_CR48","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. (2004). ASSAT: computing answer sets of a logic program by SAT solvers. Artificial Intelligence, 157, 115\u2013137.","journal-title":"Artificial Intelligence"},{"key":"9257_CR49","unstructured":"Marek, V., & Truszczy\u0144ski, M. (1999). Stable models and an alternative logic programming paradigm. In The logic programming paradigm: a 25-Year perspective (pp. 375\u2013398). Springer Verlag."},{"key":"9257_CR50","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., & Sakallah, K. A. (May 1999). GRASP: a search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5), 506\u2013521.","DOI":"10.1109\/12.769433"},{"key":"9257_CR51","unstructured":"Marques Silva, J. P., Lynce, I., & Malik, S. (2009). Conflict-driven clause learning SAT solvers. In Handbook of satisfiability (pp. 131\u2013153). IOS Press."},{"key":"9257_CR52","unstructured":"McCarthy, J. (1988). Mathematical logic in artificial intelligence. D\u00e6dalus, 297\u2013311. Reproduced in [53]."},{"key":"9257_CR53","unstructured":"McCarthy, J. (1990). Formalizing Common Sense: Papers by John McCarthy. Ablex, Norwood."},{"issue":"4\u20135","key":"9257_CR54","first-page":"465","volume":"12","author":"A Metodi","year":"2012","unstructured":"Metodi, A., & Codish, M. (2012). Compiling finite domain constraints to sat with bee*. Theory and Practice of Logic Programming, 12(4\u20135), 465\u2013483. doi: http:\/\/dx.doi.org\/10.1017\/S1471068412000130 .","journal-title":"Theory and Practice of Logic Programming"},{"key":"9257_CR55","unstructured":"Mitchell, D. G., & Ternovska, E. (2005). A framework for representing and solving np search problems. In Twentieth national conference on artificial intelligence and the seventeenth innovative applications of artificial intelligence conference (AAAI) (pp. 430\u2013435). AAAI Press \/ The MIT Press."},{"key":"9257_CR56","doi-asserted-by":"crossref","unstructured":"Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: engineering an efficient SAT solver. In Proceedings DAC-01.","DOI":"10.1145\/378239.379017"},{"key":"9257_CR57","unstructured":"Navarro-P\u00e9rez, J. (2007). Encoding and solving problems in effectively propositional logic. Ph.D. thesis, University of Manchester."},{"key":"9257_CR58","doi-asserted-by":"publisher","unstructured":"Navarro-P\u00e9rez, J., & Voronkov, A. (2013). Planning with effectively propositional logic. In Voronkov, A., & Weidenbach, C. (Eds.) Programming logics. Vol. 7797 of lecture notes in computer science. doi: 10.1007\/978-3-642-37651-1_13 (pp. 302\u2013316). Berlin Heidelberg: Springer.","DOI":"10.1007\/978-3-642-37651-1_13"},{"key":"9257_CR59","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1023\/A:1018930122475","volume":"25","author":"I Niemel\u00e4","year":"1999","unstructured":"Niemel\u00e4, I. (1999). Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence, 25, 241\u2013273.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"9257_CR60","doi-asserted-by":"crossref","unstructured":"Niemel\u00e4, I., & Simons, P. (2000). Extending the Smodels system with cardinality and weight constraints. In Minker, J (Ed.) Logic-based artificial intelligence (pp. 491\u2013521). Kluwer.","DOI":"10.1007\/978-1-4615-1567-8_21"},{"issue":"6","key":"9257_CR61","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., & Tinelli, C. (2006). Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM, 53(6), 937\u2013977.","journal-title":"Journal of the ACM"},{"key":"9257_CR62","doi-asserted-by":"crossref","unstructured":"Nogueira, M., Balduccini, M., Gelfond, M., Watson, R., & Barry, M. (2001). An A-Prolog decision support system for the Space Shuttle. In Proceedings of international symposium on practical aspects of declarative languages (PADL) (pp. 169\u2013183).","DOI":"10.1007\/3-540-45241-9_12"},{"key":"9257_CR63","doi-asserted-by":"publisher","unstructured":"Pipatsrisawat, K., & Darwiche, A. (2011). On the power of clause-learning sat solvers as resolution engines. doi: 10.1016\/j.artint.2010.10.002 , (Vol. 175 pp. 512\u2013525).","DOI":"10.1016\/j.artint.2010.10.002"},{"issue":"2","key":"9257_CR64","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"MR Prasad","year":"2005","unstructured":"Prasad, M. R., Biere, A., & Gupta, A. (2005). A survey of recent advances in SAT-based formal verification. STTT, 7(2), 156\u2013173.","journal-title":"STTT"},{"issue":"3","key":"9257_CR65","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1017\/S147106841100007X","volume":"12","author":"F Ricca","year":"2012","unstructured":"Ricca, F., Grasso, G., Alviano, M., Manna, M., Lio, V., Iiritano, S., & Leone, N. (2012). Team-building with answer set programming in the gioia-tauro seaport. Theory and Practice of Logic Programming, 12(3), 361\u2013381.","journal-title":"Theory and Practice of Logic Programming"},{"key":"9257_CR66","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/j.artint.2012.08.001","volume":"193","author":"J Rintanen","year":"2012","unstructured":"Rintanen, J. (2012). Planning as satisfiability: heuristics. Artificial Intelligence, 193, 45\u201386.","journal-title":"Artificial Intelligence"},{"key":"9257_CR67","volume-title":"Handbook of constraint programming (foundations of artificial intelligence)","author":"F Rossi","year":"2006","unstructured":"Rossi, F., Beek, P. v., & Walsh, T. (2006). Handbook of constraint programming (foundations of artificial intelligence). New York: Elsevier Science Inc."},{"key":"9257_CR68","unstructured":"Roussel, O., & Manquinho, V. M. (2009). Pseudo-boolean and cardinality constraints. In Handbook of satisfiability (pp. 695\u2013733). IOS Press."},{"issue":"1","key":"9257_CR69","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1006\/jcss.1995.1053","volume":"51","author":"J Schlipf","year":"1995","unstructured":"Schlipf, J. (1995). The expressive powers of the logic programming semantics. Journal of Computer and System Sciences, 51(1), 64\u201386. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0022000085710537 .","journal-title":"Journal of Computer and System Sciences"},{"key":"9257_CR70","unstructured":"Schulz, S. (2002). A comparison of different techniques for grounding near-propositional CNF formulae. In Proceedings of the 15th international FLAIRS conference (pp. 72\u201376)."},{"key":"9257_CR71","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., & Soininen, T. (2002). Extending and implementing the stable model semantics. Artificial Intelligence, 138, 181\u2013234.","journal-title":"Artificial Intelligence"},{"issue":"2","key":"9257_CR72","doi-asserted-by":"crossref","first-page":"211","DOI":"10.3233\/AIC-130550","volume":"26","author":"G Sutcliffe","year":"2013","unstructured":"Sutcliffe, G. (2013). The 6th IJCAR automated theorem proving system competition - CASC-J6. AI Communications, 26(2), 211\u2013223.","journal-title":"AI Communications"},{"key":"9257_CR73","doi-asserted-by":"crossref","unstructured":"Syrj\u00e4nen, T. (2001). Omega-restricted logic programs. In Proceedings of international conference on logic programming and nonmonotonic reasoning (pp. 267\u2013279).","DOI":"10.1007\/3-540-45402-0_20"},{"key":"9257_CR74","unstructured":"Syrjanen, T. (2003). Lparse manual, available at http:\/\/www.tcs.hut.fi\/Software\/smodels\/lparse.ps.gz ."},{"key":"9257_CR75","unstructured":"Ternovska, E., & Mitchell, D. G. (2009). Declarative programming of search problems with built-in arithmetic. In 21st International joint conference on artificial intelligence (IJCAI) (pp. 942\u2013947)."},{"key":"9257_CR76","unstructured":"Truszczy\u0144ski, M. (2012). Connecting first-order ASP and the logic FO(ID) through reducts. In Correct reasoning: essays on logic-based AI in honor of Vladimir Lifschitz. Springer-Verlag."},{"key":"9257_CR77","unstructured":"Tseitin, G. (1968). On the complexity of derivation in the propositional calculus. Studies in Constructive Mathematics and Mathematical Logic Part II."},{"key":"9257_CR78","unstructured":"Ward, J., & Schlipf, J. (2004). Answer set programming with clause learning. In Proceedings of international conference on logic programming and nonmonotonic reasoning (LPNMR\u201904) (pp. 302\u2013313)."},{"key":"9257_CR79","unstructured":"Wittocx, J., Mari\u00ebn, M., & Denecker, M. (2008). GidL: a grounder for FO+. In Thielscher, M., & Pagnucco, M. (Eds.) Proceedings of the twelfth international workshop on non-monotonic reasoning, international workshop on non-monotonic reasoning, Sydney, 13-15 September 2008 (pp. 189\u2013198). https:\/\/lirias. kuleuven.be\/handle\/123456789\/197022 ."},{"key":"9257_CR80","unstructured":"Wittocx, J., Mari\u00ebn, M., & Denecker, M. (2008). The idp system: a model expansion system for an extension of classical logic. In: Proceedings of workshop on logic and search, computation of structures from declarative descriptions (LaSh). electronic (pp. 153\u2013165), available at https:\/\/lirias.kuleuven.be\/bitstream\/123456789\/229814\/1\/lash08.pdf ."},{"key":"9257_CR81","unstructured":"Zhang, L., Madigan, C. F., Moskewicz, M. W., & Malik, S. (2001). Efficient conflict driven learning in a boolean satisfiability solver. In Proceedings ICCAD-01 (pp. 279\u2013285)."}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-016-9257-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-016-9257-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-016-9257-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,28]],"date-time":"2020-09-28T01:07:41Z","timestamp":1601255261000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-016-9257-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,16]]},"references-count":81,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,7]]}},"alternative-id":["9257"],"URL":"https:\/\/doi.org\/10.1007\/s10601-016-9257-7","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"type":"print","value":"1383-7133"},{"type":"electronic","value":"1572-9354"}],"subject":[],"published":{"date-parts":[[2016,12,16]]}}}