{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:28:58Z","timestamp":1725550138696},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540292081"},{"type":"electronic","value":"9783540319474"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11562931_6","type":"book-chapter","created":{"date-parts":[[2005,10,8]],"date-time":"2005-10-08T13:28:42Z","timestamp":1128778122000},"page":"37-51","source":"Crossref","is-referenced-by-count":13,"title":["On the Relation Between Answer Set and SAT Procedures (or, Between cmodels and smodels)"],"prefix":"10.1007","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Maratea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-45744-5_26","volume-title":"Automated Reasoning","author":"E. Giunchiglia","year":"2001","unstructured":"Giunchiglia, E., Maratea, M., Tacchella, A., Zambonin, D.: Evaluating search heuristics and optimization techniques in propositional satisfiability. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, p. 347. Springer, Heidelberg (2001)"},{"key":"6_CR2","unstructured":"Giunchiglia, E., Maratea, M., Lierler, Y.: SAT-based answer set programming. In: Proc. AAAI (2004)"},{"key":"6_CR3","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"2001","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press, Cambridge (2001)"},{"key":"6_CR4","first-page":"51","volume":"1","author":"F. Fages","year":"1994","unstructured":"Fages, F.: Consistency of Clark\u2019s completion and existence of stable models. Journal of Methods of Logic in Computer Science\u00a01, 51\u201360 (1994)","journal-title":"Journal of Methods of Logic in Computer Science"},{"key":"6_CR5","unstructured":"Babovich, Y., Lifschitz, V.: Computing Answer Sets Using Program Completion (2003), http:\/\/www.cs.utexas.edu\/users\/tag\/cmodels\/cmodels-1.ps"},{"key":"6_CR6","unstructured":"Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by SAT solvers. In: Proc. AAAI (2002)"},{"key":"6_CR7","unstructured":"Simons, P.: Extending and implementing the stable model semantics. PhD Thesis (2000)"},{"key":"6_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-540-24609-1_26","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"J. Ward","year":"2003","unstructured":"Ward, J., Schlipf, J.S.: Answer set programming with clause learning. In: Lifschitz, V., Niemel\u00e4, I. (eds.) LPNMR 2004. LNCS (LNAI), vol.\u00a02923, pp. 302\u2013313. Springer, Heidelberg (2003)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Haken: The intractability of resolution. TCS\u00a039, 297\u2013308 (1985)","DOI":"10.1016\/0304-3975(85)90144-6"},{"issue":"4","key":"6_CR10","doi-asserted-by":"publisher","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chv\u00e1tal","year":"1988","unstructured":"Chv\u00e1tal, V., Szemer\u00e9di, E.: Many hard examples for resolution. J. ACM\u00a035(4), 759\u2013768 (1988)","journal-title":"J. ACM"},{"key":"6_CR11","unstructured":"Faber, W., Leone, N., Pfeifer, G.: Experimenting with heuristics for ASP. In: Proc. IJCAI (2001)"},{"issue":"1\u20132","key":"6_CR12","doi-asserted-by":"publisher","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. Artificial Intelligence\u00a0138(1\u20132), 181\u2013234 (2002)","journal-title":"Artificial Intelligence"},{"issue":"1-2","key":"6_CR13","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/S0004-3702(99)00097-1","volume":"116","author":"P. Liberatore","year":"2000","unstructured":"Liberatore, P.: On the complexity of choosing the branching literal in DPLL. Artificial Intelligence\u00a0116(1-2), 315\u2013326 (2000)","journal-title":"Artificial Intelligence"},{"key":"6_CR14","series-title":"Lecture Notes in Physics","first-page":"232","volume-title":"Complex Networks","author":"R. Monasson","year":"2004","unstructured":"Monasson, R.: On the analysis of backtrack procedures for the coloring of random graphs. In: Complex Networks. Lecture Notes in Physics, pp. 232\u2013251. Springer, Heidelberg (2004)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Achlioptas, D., Beame, P., Molloy, M.: A sharp threshold in proof complexity. In: Proc. STOC, pp. 337\u2013346 (2001)","DOI":"10.1145\/380752.380820"},{"key":"6_CR16","unstructured":"Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proc. IJCAI (1997)"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. DAC (2001)","DOI":"10.1145\/378239.379017"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Le Berre, D., Simon, L.: The essentials of the SAT 2003 competition. In: Proc. SAT (2003)","DOI":"10.1007\/978-3-540-24605-3_34"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Lin, F., Zhao, Y.: ASP phase transition: A study on randomly generated programs. In: Proc. ICLP (2003)","DOI":"10.1007\/978-3-540-24599-5_17"},{"key":"6_CR20","doi-asserted-by":"publisher","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. Annals of Mathematics and Artificial Intelligence\u00a025, 241\u2013273 (1999)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Dixon, H., Ginsberg, M., Luks, E., Parkes, A.: Generalizing Boolean satisfiability II: Theory. In: JAIR, vol.\u00a022, pp. 481\u2013534 (2004)","DOI":"10.1613\/jair.1555"},{"key":"6_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-24609-1_3","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"P. Borchert","year":"2003","unstructured":"Borchert, P., Anger, C., Schaub, T., Truszczynski, M.: Towards systematic benchmarking in answer set programming: The dagstuhl initiative. In: Lifschitz, V., Niemel\u00e4, I. (eds.) LPNMR 2004. LNCS (LNAI), vol.\u00a02923, pp. 3\u20137. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11562931_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:52:13Z","timestamp":1605642733000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11562931_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540292081","9783540319474"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11562931_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}