{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:32:49Z","timestamp":1761611569101,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":61,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642307423"},{"type":"electronic","value":"9783642307430"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30743-0_22","type":"book-chapter","created":{"date-parts":[[2012,6,2]],"date-time":"2012-06-02T03:49:46Z","timestamp":1338608986000},"page":"327-344","source":"Crossref","is-referenced-by-count":0,"title":["Algorithms for Solving Satisfiability Problems with Qualitative Preferences"],"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":"22_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Generic ILP versus specialized 0-1 ILP: an update. In: Pileggi, L.T., Kuehlmann, A. (eds.) Proc. of the 2002 IEEE\/ACM International Conference on Computer-aided Design (ICCAD 2002), pp. 450\u2013457. ACM (2002)","DOI":"10.1145\/774572.774638"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Amgoud, L., Cayrol, C., LeBerre, D.: Comparing arguments using preference ordering for argument-based reasoning. In: Proc. of the 8th International Conference on Tools with Artificial Intelligence (ICTAI 1996), pp. 400\u2013403. IEEE Computer Society (1996)","DOI":"10.1109\/TAI.1996.560731"},{"key":"22_CR3","unstructured":"Bienvenu, M., Lang, J., Wilson, N.: From preference logics to preference languages, and back. In: Lin, F., Sattler, U., Truszczynski, M. (eds.) Proc. of the 12th International Conference on Principles of Knowledge Representation and Reasoning (KR 2010). AAAI Press (2010)"},{"key":"22_CR4","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1613\/jair.1234","volume":"21","author":"C. Boutilier","year":"2004","unstructured":"Boutilier, C., Brafman, R.I., Domshlak, C., Hoos, H.H., Poole, D.: CP-nets: A tool for representing and reasoning with conditional ceteris paribus preference statements. Journal of Artificial Intelligence Research\u00a021, 135\u2013191 (2004)","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"2","key":"22_CR5","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1111\/j.0824-7935.2004.00234.x","volume":"20","author":"C. Boutilier","year":"2004","unstructured":"Boutilier, C., Brafman, R.I., Domshlak, C., Hoos, H.H., Poole, D.: Preference-based constrained optimization with CP-nets. Computational Intelligence\u00a020(2), 137\u2013157 (2004)","journal-title":"Computational Intelligence"},{"key":"22_CR6","unstructured":"Brewka, G.: Logic programming with ordered disjunction. In: Dechter, R., Sutton, R.S. (eds.) Proc. of the 18th National Conference on Artificial Intelligence (AAAI 2002), pp. 100\u2013105. AAAI Press \/ The MIT Press (2002)"},{"key":"22_CR7","unstructured":"Brewka, G.: Complex preferences for answer set optimization. In: Dubois, D., Welty, C.A., Williams, M.-A. (eds.) Proc. of the 9th International Conference on Principles of Knowledge Representation and Reasoning (KR 2004), pp. 213\u2013223. AAAI Press (2004)"},{"issue":"1-2","key":"22_CR8","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/S0004-3702(99)00015-6","volume":"109","author":"G. Brewka","year":"1999","unstructured":"Brewka, G., Eiter, T.: Preferred answer sets for extended logic programs. Artificial Intelligence\u00a0109(1-2), 297\u2013356 (1999)","journal-title":"Artificial Intelligence"},{"issue":"2","key":"22_CR9","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1111\/j.0824-7935.2004.00241.x","volume":"20","author":"G. Brewka","year":"2004","unstructured":"Brewka, G., Niemel\u00e4, I., Syrj\u00e4nen, T.: Logic programs with ordered disjunction. Computational Intelligence\u00a020(2), 335\u2013357 (2004)","journal-title":"Computational Intelligence"},{"key":"22_CR10","unstructured":"Brewka, G., Niemel\u00e4, I., Truszczynski, M.: Answer set optimization. In: Gottlob, G., Walsh, T. (eds.) Proc. of the 18th International Joint Conference on Artificial Intelligence (IJCAI 2003), pp. 867\u2013872. Morgan Kaufmann (2003)"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-63255-7_2","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"F. Buccafurri","year":"1997","unstructured":"Buccafurri, F., Leone, N., Rullo, P.: Strong and Weak Constraints in Disjunctive Datalog. In: Fuhrbach, U., Dix, J., Nerode, A. (eds.) LPNMR 1997. LNCS, vol.\u00a01265, pp. 2\u201317. Springer, Heidelberg (1997)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/978-3-642-04238-6_36","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"D. \u00c7akmak","year":"2009","unstructured":"\u00c7akmak, D., Erdem, E., Erdo\u011fan, H.: Computing Weighted Solutions in Answer Set Programming. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol.\u00a05753, pp. 416\u2013422. Springer, Heidelberg (2009)"},{"key":"22_CR13","first-page":"350","volume-title":"Proc. of the 12th European Conference on Artificial Intelligence (ECAI 1996)","author":"T. Castell","year":"1996","unstructured":"Castell, T., Cayrol, C., Cayrol, M., Le Berre, D.: Using the Davis and Putnam procedure for an efficient computation of preferred models. In: Wahlster, W. (ed.) Proc. of the 12th European Conference on Artificial Intelligence (ECAI 1996), pp. 350\u2013354. John Wiley and Sons, Chichester (1996)"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Coudert, O.: On solving covering problems. In: Pennino, T., Yoffa, E.J. (eds.) Proc. of the 33rd Conference on Design Automation (DAC 1996), pp. 197\u2013202. ACM Press (1996)","DOI":"10.1145\/240518.240555"},{"issue":"7","key":"22_CR15","doi-asserted-by":"publisher","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. Communication of ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communication of ACM"},{"key":"22_CR16","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"issue":"1-2","key":"22_CR17","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/S0004-3702(00)00049-7","volume":"123","author":"J.P. Delgrande","year":"2000","unstructured":"Delgrande, J.P., Schaub, T.: Expressing preferences in default logic. Artificial Intelligence\u00a0123(1-2), 41\u201387 (2000)","journal-title":"Artificial Intelligence"},{"issue":"2","key":"22_CR18","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1111\/j.0824-7935.2004.00240.x","volume":"20","author":"J.P. Delgrande","year":"2004","unstructured":"Delgrande, J.P., Schaub, T., Tompits, H., Wang, K.: A classification and survey of preference handling approaches in nonmonotonic reasoning. Computational Intelligence\u00a020(2), 308\u2013334 (2004)","journal-title":"Computational Intelligence"},{"key":"22_CR19","unstructured":"DiRosa, E., Giunchiglia, E., Maratea, M.: A new approach for solving satisfiability problems with qualitative preferences. In: Ghallab, M., Spyropoulos, C.D., Fakotakis, N., Avouris, N.M. (eds.) Proc. of the 18th European Conference on Artificial Intelligence (ECAI 2008). Frontiers in AI and Applications, vol.\u00a0178, pp. 510\u2013514. IOS Press (2008)"},{"issue":"4","key":"22_CR20","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/s10601-010-9095-y","volume":"15","author":"E. DiRosa","year":"2010","unstructured":"DiRosa, E., Giunchiglia, E., Maratea, M.: Solving satisfiability problems with preferences. Constraints\u00a015(4), 485\u2013515 (2010)","journal-title":"Constraints"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"DiRosa, E., Giunchiglia, E., O\u2019Sullivan, B.: Optimal stopping methods for finding high quality solutions to satisfiability problems with preferences. In: Chu, W.C., Eric Wong, W., Palakal, M.J., Hung, C.-C. (eds.) Proc. of the 2011 ACM Symposium on Applied Computing (SAC 2011), pp. 901\u2013906. ACM (2011)","DOI":"10.1145\/1982185.1982382"},{"key":"22_CR22","unstructured":"Doyle, J., Junker, U.: Preferences. In: Tutotial at the 19th National Conference on Artificial Intelligence, AAAI 2004 (2004)"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective Preprocessing in SAT Through Variable and Clause Elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"4-5","key":"22_CR25","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1017\/S1471068403001753","volume":"3","author":"T. Eiter","year":"2003","unstructured":"Eiter, T., Faber, W., Leone, N., Pfeifer, G.: Computing preferred answer sets by meta-interpretation in answer set programming. Theory and Practice of Logic Programming\u00a03(4-5), 463\u2013498 (2003)","journal-title":"Theory and Practice of Logic Programming"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"763","DOI":"10.1007\/3-540-45578-7_64","volume-title":"Principles and Practice of Constraint Programming - CP 2001","author":"M. Gavanelli","year":"2001","unstructured":"Gavanelli, M.: Partially Ordered Constraint Optimization Problems. In: Walsh, T. (ed.) CP 2001. LNCS, vol.\u00a02239, p. 763. Springer, Heidelberg (2001)"},{"key":"22_CR27","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Multi-criteria optimization in answer set programming. In: Gallagherand, J.P., Gelfond, M. (eds.) Technical Communications of the 27th International Conference on Logic Programming (ICLP 2011). LIPIcs, vol.\u00a011, pp. 1\u201310. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)"},{"issue":"4-5","key":"22_CR28","doi-asserted-by":"publisher","first-page":"821","DOI":"10.1017\/S1471068411000329","volume":"11","author":"M. Gebser","year":"2011","unstructured":"Gebser, M., Kaminski, R., Schaub, T.: Complex optimization in answer set programming. Theory and Practice of Logic Programming\u00a011(4-5), 821\u2013839 (2011)","journal-title":"Theory and Practice of Logic Programming"},{"key":"22_CR29","unstructured":"Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In: Veloso, M.M. (ed.) Proc. of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 386\u2013391 (2007)"},{"key":"22_CR30","unstructured":"Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R., Bowen, K. (eds.) Proc. of the 5th International Conference and Symposium on Logic Programming (ICLP\/SLP 1988), pp. 1070\u20131080 (1988)"},{"key":"22_CR31","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\u2013385 (1991)","journal-title":"New Generation Computing"},{"key":"22_CR32","unstructured":"Gent, I., Van Maaren, H., Walsh, T. (eds.): SAT 2000. Satisfiability Research in the Year 2000. IOS Press (2000)"},{"key":"22_CR33","doi-asserted-by":"publisher","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. Journal of Automated Reasoning\u00a028, 143\u2013171 (2002), Reprinted in [32]","journal-title":"Journal of Automated Reasoning"},{"key":"22_CR34","unstructured":"Giunchiglia, E., Maratea, M.: Solving optimization problems with DLL. In: Brewka, G., Coradeschi, S., Perini, A., Traverso, P. (eds.) Proc. of the 17th European Conference on Artificial Intelligence (ECAI 2006). Frontiers in Artificial Intelligence and Applications, vol.\u00a0141, pp. 377\u2013381. IOS Press (2006)"},{"key":"22_CR35","unstructured":"Giunchiglia, E., Massarotto, A., Sebastiani, R.: Act, and the rest will follow: Exploiting determinism in planning as satisfiability. In: Mostow, J., Rich, C. (eds.) Proc. of the 15th National Conference on Artificial Intelligence (AAAI 1998), pp. 948\u2013953. AAAI Press \/ The MIT Press (1998)"},{"key":"22_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-45193-8_25","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"S. Givry de","year":"2003","unstructured":"de Givry, S., Larrosa, J., Meseguer, P., Schiex, T.: Solving Max-SAT as Weighted CSP. In: Rossi, F. (ed.) CP 2003. LNCS, vol.\u00a02833, pp. 363\u2013376. Springer, Heidelberg (2003)"},{"key":"22_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/11527695_15","volume-title":"Theory and Applications of Satisfiability Testing","author":"P. Jackson","year":"2005","unstructured":"Jackson, P., Sheridan, D.: Clause Form Conversions for Boolean Circuits. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 183\u2013198. Springer, Heidelberg (2005)"},{"issue":"4","key":"22_CR38","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/s10472-005-7034-1","volume":"44","author":"M. J\u00e4rvisalo","year":"2005","unstructured":"J\u00e4rvisalo, M., Junttila, T., Niemel\u00e4, I.: Unrestricted vs restricted cut in a tableau method for Boolean circuits. Annals of Mathematics and Artificial Intelligence\u00a044(4), 373\u2013399 (2005)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"3","key":"22_CR39","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10601-008-9062-z","volume":"14","author":"M. J\u00e4rvisalo","year":"2009","unstructured":"J\u00e4rvisalo, M., Junttila, T.A.: Limitations of restricted branching in clause learning. Constraints\u00a014(3), 325\u2013356 (2009)","journal-title":"Constraints"},{"key":"22_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-31980-1_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Jin","year":"2005","unstructured":"Jin, H., Han, H., Somenzi, F.: Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 287\u2013300. Springer, Heidelberg (2005)"},{"key":"22_CR41","doi-asserted-by":"crossref","unstructured":"Jin, H., Somenzi, F.: Prime clauses for fast enumeration of satisfying assignments to Boolean circuits. In: Joyner Jr., W.H., Martin, G., Kahng, A.B. (eds.) Proc. of the 42nd Design Automation Conference (DAC 2005), pp. 750\u2013753. ACM (2005)","DOI":"10.1145\/1065579.1065775"},{"key":"22_CR42","unstructured":"Kautz, H., Selman, B.: Planning as satisfiability. In: Neumann, B. (ed.) Proc. of the 10th European Conference on Artificial Intelligence (ECAI 1992), pp. 359\u2013363. John Wiley and Sons (1992)"},{"issue":"3","key":"22_CR43","doi-asserted-by":"publisher","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.: The DLV system for knowledge representation and reasoning. ACM Transactions on Computational Logic\u00a07(3), 499\u2013562 (2006)","journal-title":"ACM Transactions on Computational Logic"},{"key":"22_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-642-02777-2_45","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"V. Manquinho","year":"2009","unstructured":"Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for Weighted Boolean Optimization. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 495\u2013508. Springer, Heidelberg (2009)"},{"key":"22_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-15675-5_33","volume-title":"Logics in Artificial Intelligence","author":"M. Maratea","year":"2010","unstructured":"Maratea, M., Ricca, F., Veltri, P.: DLV MC Enhanced Model Checking in DLV. In: Janhunen, T., Niemel\u00e4, I. (eds.) JELIA 2010. LNCS, vol.\u00a06341, pp. 365\u2013368. Springer, Heidelberg (2010)"},{"key":"22_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT Methods in Unbounded Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 250\u2013264. Springer, Heidelberg (2002)"},{"key":"22_CR47","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking: an Approach to the State Explosion Problem. Kluwer Academic Publishers (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"22_CR48","first-page":"112","volume":"85","author":"D.G. Mitchell","year":"2005","unstructured":"Mitchell, D.G.: A SAT solver Primer. Bulletin of the EATCS\u00a085, 112\u2013132 (2005)","journal-title":"Bulletin of the EATCS"},{"issue":"1-2","key":"22_CR49","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1017\/S1471068404002315","volume":"6","author":"D. Nieuwenborgh Van","year":"2006","unstructured":"Van Nieuwenborgh, D., Vermeir, D.: Preferred answer sets for ordered logic programs. Theory and Practice of Logic Programming\u00a06(1-2), 107\u2013167 (2006)","journal-title":"Theory and Practice of Logic Programming"},{"key":"22_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-642-04238-6_21","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"E. Oikarinen","year":"2009","unstructured":"Oikarinen, E., J\u00e4rvisalo, M.: Max-ASP: Maximum Satisfiability of Answer Set Programs. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol.\u00a05753, pp. 236\u2013249. Springer, Heidelberg (2009)"},{"key":"22_CR51","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. Journal of Symbolic Computation\u00a02, 293\u2013304 (1986)","journal-title":"Journal of Symbolic Computation"},{"key":"22_CR52","unstructured":"Prestwich, S.: Three implementation of branch-and-cut in CLP. In: Proc. of the 4th Compulog-Net Workshop on Parallelism and Implementation Technologies (1996)"},{"key":"22_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/978-3-540-74970-7_43","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"M. Ram\u00edrez","year":"2007","unstructured":"Ram\u00edrez, M., Geffner, H.: Structural Relaxations by Variable Renaming and Their Compilation for Solving MinCostSAT. In: Bessiere, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 605\u2013619. Springer, Heidelberg (2007)"},{"key":"22_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-540-24730-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Ravi","year":"2004","unstructured":"Ravi, K., Somenzi, F.: Minimal Assignments for Bounded Model Checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 31\u201345. Springer, Heidelberg (2004)"},{"key":"22_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-642-20895-9_21","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"E. Saad","year":"2011","unstructured":"Saad, E., Brewka, G.: Aggregates in Answer Set Optimization. In: Delgrande, J.P., Faber, W. (eds.) LPNMR 2011. LNCS, vol.\u00a06645, pp. 211\u2013216. Springer, Heidelberg (2011)"},{"key":"22_CR56","doi-asserted-by":"crossref","unstructured":"Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970, vol.\u00a01-2. Springer (1983)","DOI":"10.1007\/978-3-642-81955-1"},{"key":"22_CR57","doi-asserted-by":"crossref","unstructured":"Marques Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 131\u2013153. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-131"},{"issue":"1\u20132","key":"22_CR58","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"},{"key":"22_CR59","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of proofs in propositional logics. Seminars in Mathematics\u00a08 (1970) Reprinted in [56]","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"22_CR60","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/3-540-44957-4_11","volume-title":"Computational Logic - CL 2000","author":"K. Wang","year":"2000","unstructured":"Wang, K., Zhou, L., Lin, F.: Alternating Fixpoint Theory for Logic Programs with Priority. In: Lloyd, J., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Palamidessi, C., Moniz Pereira, L., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 164\u2013178. Springer, Heidelberg (2000)"},{"issue":"2","key":"22_CR61","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"J.P. Warners","year":"1998","unstructured":"Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters\u00a068(2), 63\u201369 (1998)","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Correct Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30743-0_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,29]],"date-time":"2025-03-29T06:44:12Z","timestamp":1743230652000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30743-0_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642307423","9783642307430"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30743-0_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}