{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:53:48Z","timestamp":1725551628366},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540305538"},{"type":"electronic","value":"9783540316503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11591191_39","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T09:44:25Z","timestamp":1132652665000},"page":"565-579","source":"Crossref","is-referenced-by-count":5,"title":["Satisfiability Checking for PC(ID)"],"prefix":"10.1007","author":[{"given":"Maarten","family":"Mari\u00ebn","sequence":"first","affiliation":[]},{"given":"Rudradeb","family":"Mitra","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Denecker","sequence":"additional","affiliation":[]},{"given":"Maurice","family":"Bruynooghe","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"39_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/3-540-59487-6_9","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"K.A. Berman","year":"1995","unstructured":"Berman, K.A., Schlipf, J.S., Franco, J.V.: Computing the well-founded semantics faster. In: Marek, V.W., Truszczy\u0144ski, M., Nerode, A. (eds.) LPNMR 1995. LNCS, vol.\u00a0928, pp. 113\u2013126. Springer, Heidelberg (1995)"},{"key":"39_CR2","unstructured":"Brachman, R.J., Levesque, H.J.: Competence in knowledge representation. In: Proc. of the National Conference on Artificial Intelligence, pp. 189\u2013192 (1982)"},{"key":"39_CR3","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Longemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"39_CR4","series-title":"Lecture Notes in Artificial Intelligence","first-page":"424","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"T. Dell\u2019Armi","year":"2001","unstructured":"Dell\u2019Armi, T., Faber, W., Ielpa, G., Koch, C., Leone, N., Perri, S., Pfeifer, G.: System description: DLV. In: Eiter, T., Faber, W., Truszczy\u0144ski, M. (eds.) LPNMR 2001. LNCS (LNAI), vol.\u00a02173, pp. 424\u2013428. Springer, Heidelberg (2001)"},{"key":"39_CR5","unstructured":"Denecker, M.: Knowledge Representation and Reasoning in Incomplete Logic Programming. PhD thesis, Department of Computer Science, K.U.Leuven (1993)"},{"key":"39_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-49545-2_1","volume-title":"Logics in Artificial Intelligence","author":"M. Denecker","year":"1998","unstructured":"Denecker, M.: The well-founded semantics is the principle of inductive definition. In: Dix, J., Fari\u00f1as del Cerro, L., Furbach, U. (eds.) JELIA 1998. LNCS (LNAI), vol.\u00a01489, pp. 1\u201316. Springer, Heidelberg (1998)"},{"key":"39_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/3-540-44957-4_47","volume-title":"Computational Logic - CL 2000","author":"M. Denecker","year":"2000","unstructured":"Denecker, M.: Extending classical logic with inductive definitions. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 703\u2013717. Springer, Heidelberg (2000)"},{"issue":"4","key":"39_CR8","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1145\/383779.383789","volume":"2","author":"M. Denecker","year":"2001","unstructured":"Denecker, M., Bruynooghe, M., Marek, V.: Logic programming revisited: logic programs as inductive definitions. ACM Transactions on Computational Logic\u00a02(4), 623\u2013654 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"39_CR9","first-page":"365","volume-title":"LPNMR","author":"M. Denecker","year":"1993","unstructured":"Denecker, M., De Schreye, D.: Justification semantics: a unifying framework for the semantics of logic programs. In: LPNMR, pp. 365\u2013379. MIT Press, Cambridge (1993)"},{"key":"39_CR10","first-page":"545","volume-title":"KR","author":"M. Denecker","year":"2004","unstructured":"Denecker, M., Ternovska, E.: Inductive situation calculus. In: Dubois, D., Welty, C.A., Williams, M. (eds.) KR, pp. 545\u2013553. AAAI Press, Menlo Park (2004)"},{"key":"39_CR11","unstructured":"East, D., Truszczy\u0144ski, M.: dcs: An implementation of datalog with constraints. CoRR, cs.AI\/0003061 (2000)"},{"key":"39_CR12","doi-asserted-by":"publisher","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 Generation Computing\u00a09, 365\u2013387 (1991)","journal-title":"New Generation Computing"},{"key":"39_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-24609-1_32","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"Y. Lierler","year":"2003","unstructured":"Lierler, Y., Maratea, M.: Cmodels-2: SAT-based answer set solver enhanced to non-tight programs. In: Lifschitz, V., Niemel\u00e4, I. (eds.) LPNMR 2004. LNCS (LNAI), vol.\u00a02923, pp. 346\u2013350. Springer, Heidelberg (2003)"},{"issue":"1-2","key":"39_CR14","doi-asserted-by":"publisher","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.\u00a0157(1-2), 115\u2013137 (2004)","journal-title":"Artif. Intell."},{"key":"39_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"673","DOI":"10.1007\/3-540-44957-4_45","volume-title":"Computational Logic - CL 2000","author":"Z. Lonc","year":"2000","unstructured":"Lonc, Z., Truszczy\u0144ski, M.: On the problem of computing the well-founded semantics. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 673\u2013687. Springer, Heidelberg (2000)"},{"key":"39_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30227-8_12","volume-title":"Logics in Artificial Intelligence","author":"M. Mari\u00ebn","year":"2004","unstructured":"Mari\u00ebn, M., Gilis, D., Denecker, M.: On the relation between ID-logic and answer set programming. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS, vol.\u00a03229, pp. 108\u2013120. Springer, Heidelberg (2004)"},{"key":"39_CR17","doi-asserted-by":"crossref","unstructured":"Mari\u00ebn, M., Mitra, R., Denecker, M., Bruynooghe, M.: Satisfiability checking for PC(ID). Technical Report CW426, K.U. Leuven (2005)","DOI":"10.1007\/11591191_39"},{"issue":"5","key":"39_CR18","doi-asserted-by":"publisher","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. Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Computers"},{"key":"39_CR19","unstructured":"Mitchell, D.G., Ternovska, E.: A framework for representing and solving NP search problems. In: Twentieth National Conf. on Artificial Intelligence (AAAI 2005). AAAI\u00a0Press\/MIT Press (2005)"},{"key":"39_CR20","first-page":"530","volume-title":"DAC","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC, pp. 530\u2013535. ACM, New York (2001)"},{"key":"39_CR21","unstructured":"Niemel\u00e4, I., Simons, P., Syrj\u00e4nen, T.: Smodels: a system for answer set programming. In: NMR (2000)"},{"issue":"1","key":"39_CR22","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/0020-0190(94)90047-7","volume":"49","author":"E. Nuutila","year":"1994","unstructured":"Nuutila, E., Soisalon-Soininen, E.: On finding the strongly connected components in a directed graph. Inf. Process. Lett.\u00a049(1), 9\u201314 (1994)","journal-title":"Inf. Process. Lett."},{"key":"39_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11562931_18","volume-title":"Logic Programming","author":"N. Pelov","year":"2005","unstructured":"Pelov, N., Ternovska, E.: Reducing inductive definitions to propositional satisfiability. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol.\u00a03668, pp. 221\u2013234. Springer, Heidelberg (2005)"},{"key":"39_CR24","unstructured":"Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Master\u2019s thesis, Simon Fraser University (2004)"},{"key":"39_CR25","first-page":"442","volume-title":"SIGMOD Conference","author":"K.F. Sagonas","year":"1994","unstructured":"Sagonas, K.F., Swift, T., Warren, D.S.: XSB as an efficient deductive database engine. In: Snodgrass, R.T., Winslett, M. (eds.) SIGMOD Conference, pp. 442\u2013453. ACM Press, New York (1994)"},{"issue":"2","key":"39_CR26","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput.\u00a01(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"39_CR27","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0022-0000(93)90024-Q","volume":"47","author":"A. Van Gelder","year":"1993","unstructured":"Van Gelder, A.: The alternating fixpoint of logic programs with negation. Journal of Computer and System Sciences\u00a047(1), 185\u2013221 (1993)","journal-title":"Journal of Computer and System Sciences"},{"issue":"3","key":"39_CR28","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1145\/116825.116838","volume":"38","author":"A. Van Gelder","year":"1991","unstructured":"Van Gelder, A., Ross, K.A., Schlipf, J.S.: The well-founded semantics for general logic programs. Journal of the ACM\u00a038(3), 620\u2013650 (1991)","journal-title":"Journal of the ACM"},{"key":"39_CR29","first-page":"279","volume-title":"ICCAD","author":"L. Zhang","year":"2001","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: ICCAD, pp. 279\u2013285. ACM, New York (2001)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11591191_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:02:30Z","timestamp":1605643350000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11591191_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540305538","9783540316503"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/11591191_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}