{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:27:08Z","timestamp":1725575228840},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540207214"},{"type":"electronic","value":"9783540246091"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-24609-1_26","type":"book-chapter","created":{"date-parts":[[2011,1,14]],"date-time":"2011-01-14T03:31:31Z","timestamp":1294975891000},"page":"302-313","source":"Crossref","is-referenced-by-count":17,"title":["Answer Set Programming with Clause Learning"],"prefix":"10.1007","author":[{"given":"Jeffrey","family":"Ward","sequence":"first","affiliation":[]},{"given":"John S.","family":"Schlipf","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"Babovich, Y., Erdem, E., Lifschitz, V.: Fage\u2019s Theorem and Answer Set Programming. In: Proc. Int\u2019l. Workshop on Non-Monotonic Reasoning (2000)","key":"26_CR1"},{"unstructured":"Babovich, Y., Maratea, M.: Cmodels-2: SAT-based Answer Set Solver Enhanced to Non-tight Programs, Available from http:\/\/www.cs.utexas.edu\/users\/tag\/cmodels.html","key":"26_CR2"},{"doi-asserted-by":"crossref","unstructured":"Bayardo, R., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proc. of the Int\u2019l. Conf. on Automate Deduction (1997)","key":"26_CR3","DOI":"10.1007\/3-540-61551-2_65"},{"key":"26_CR4","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 Press, New York (1978)"},{"key":"26_CR5","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.: A Machine Program for Theorem Proving. Communications of the Association of Computing Machinery\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the Association of Computing Machinery"},{"doi-asserted-by":"crossref","unstructured":"Eiter, T., Faber, W., Leone, N., Pfeifer, G.: Declarative Problem-Solving Using the DLV System. In: Minker, J. (ed.) Logic-Based Artificial Intelligence, pp. 79\u2013103 (2000)","key":"26_CR6","DOI":"10.1007\/978-1-4615-1567-8_4"},{"key":"26_CR7","first-page":"51","volume":"1","author":"F. Fages","year":"1994","unstructured":"Fages, F.: Consistency of Clark\u2019s completion and existence of stable models. J. Methods of Logic in Computer Science\u00a01, 51\u201360 (1994)","journal-title":"J. Methods of Logic in Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Maratea, M., Tacchella, A.: Look-Ahead vs. Look-Back techniques in a modern SAT solver. In: SAT 2003, Portofino, Italy, May 5-8 (2003)","key":"26_CR8","DOI":"10.1007\/978-3-540-45193-8_64"},{"doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a Fast and Robust Sat\u2013Solver. Design Automation and Test in Europe (DATE), 142\u2013149 (2002)","key":"26_CR9","DOI":"10.1109\/DATE.2002.998262"},{"unstructured":"Lin, F., Jicheng, Z.: On Tight Logic Programs and Yet Another Translation from Normal Logic Programs to Propositional Logic. In: Proc. of IJCAI 2003 (2003) (to appear)","key":"26_CR10"},{"unstructured":"Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by SAT solvers. In: Proc. of the 18th Nat\u2019l. Conf. on Artificial Intelligence, AAAI 2002 (2002)","key":"26_CR11"},{"issue":"5","key":"26_CR12","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans. on Computers 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. on Computers"},{"doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. of the 38th Design Automation Conf., DAC 2001 (2001)","key":"26_CR13","DOI":"10.1145\/378239.379017"},{"unstructured":"Niemela, I., Simons, P., Syrjanen, T.: Smodels: a system for answer set programming. In: Proc. of the 8th Int\u2019l. Workshop on Non-Monotonic Reasoning (2000)","key":"26_CR14"},{"issue":"3-4","key":"26_CR15","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1023\/A:1018930122475","volume":"25","author":"I. Niemela","year":"1999","unstructured":"Niemela, I.: Logic programming with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence\u00a025(3-4), 241\u2013273 (1999)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"unstructured":"Simons, P.: Extending and Implementing the Stable Model Semantics. PhD dissertation, Helsinki University of Technology (2000)","key":"26_CR16"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-48153-2_5","volume-title":"Correct Hardware Design and Verification Methods","author":"M. Velev","year":"1999","unstructured":"Velev, M., Bryant, R.: Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 37\u201353. Springer, Heidelberg (1999)"},{"doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: An Efficient Propositional Prover. In: Proc. of Int\u2019l. Conf. on Automated Deduction (1997)","key":"26_CR18","DOI":"10.1007\/3-540-63104-6_28"},{"doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. In: Proc. of ICCAD 2001 (2001)","key":"26_CR19","DOI":"10.1145\/774572.774637"},{"unstructured":"ASSAT code, available from http:\/\/assat.cs.ust.hk\/","key":"26_CR20"},{"unstructured":"Cmodels code, available from http:\/\/www.cs.utexas.edu\/users\/tag\/cmodels.html","key":"26_CR21"},{"unstructured":"Chaff2 code, available from http:\/\/www.ee.princeton.edu\/chaff\/index1.html","key":"26_CR22"},{"unstructured":"Simo code is included in the Cmodels-2 distribution, See also http:\/\/www.mrg.dist.unige.it\/sim\/simo\/","key":"26_CR23"}],"container-title":["Lecture Notes in Computer Science","Logic Programming and Nonmonotonic Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24609-1_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T20:53:09Z","timestamp":1559940789000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24609-1_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540207214","9783540246091"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24609-1_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}