{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T02:47:14Z","timestamp":1768445234833,"version":"3.49.0"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2010,7,3]],"date-time":"2010-07-03T00:00:00Z","timestamp":1278115200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2010,10]]},"DOI":"10.1007\/s10601-010-9095-y","type":"journal-article","created":{"date-parts":[[2010,7,2]],"date-time":"2010-07-02T10:35:49Z","timestamp":1278066949000},"page":"485-515","source":"Crossref","is-referenced-by-count":40,"title":["Solving satisfiability problems with preferences"],"prefix":"10.1007","volume":"15","author":[{"given":"Emanuele","family":"Di Rosa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Giunchiglia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Maratea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,7,3]]},"reference":[{"key":"9095_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F. A., Ramani, A., Markov, I. L., & Sakallah, K. A. (2002). Generic ILP versus specialized 0-1 ILP: An update. In Proc. ICCAD (pp. 450\u2013457).","DOI":"10.1145\/774572.774638"},{"key":"9095_CR2","unstructured":"Aloul, F. A., Ramani, A., Markov, I. L., & Sakallah, K. A. (2002). PBS: A backtrack search Pseudo-Boolean solver. In Proc. SAT."},{"key":"9095_CR3","doi-asserted-by":"crossref","unstructured":"Amgoud, L., Cayrol, C., & Le Berre, D. (1996). Comparing arguments using preference ordering for argument-based reasoning. In Proc. ICTAI (pp. 400\u2013403).","DOI":"10.1109\/TAI.1996.560731"},{"key":"9095_CR4","doi-asserted-by":"crossref","unstructured":"Bailleux, O., & Boufkhad, Y. (2003). Efficient CNF encoding of Boolean cardinality constraints. In Proc. CP (pp. 108\u2013122).","DOI":"10.1007\/978-3-540-45193-8_8"},{"key":"9095_CR5","unstructured":"Barth, P. (1995). A Davis-Putnam enumeration algorithm for linear Pseudo-Boolean optimization. Technical report, Max Plank Institute for Computer Science, MPI-I-95-2-2003."},{"key":"9095_CR6","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., & Zhu, Y. (1999). Symbolic model checking without BDDs. In Proc. TACAS.","DOI":"10.21236\/ADA360973"},{"issue":"4","key":"9095_CR7","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1023\/A:1009725216438","volume":"2","author":"B Borchers","year":"1998","unstructured":"Borchers, B., & Furman, J. (1998). A two-phase exact algorithm for Max-SAT and weighted Max-SAT problems. Journal of Combinatorial Optimization, 2(4), 299\u2013306.","journal-title":"Journal of Combinatorial Optimization"},{"issue":"2","key":"9095_CR8","doi-asserted-by":"crossref","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. (2004). Preference-based constrained optimization with CP-nets. Computational Intelligence, 20(2), 137\u2013157.","journal-title":"Computational Intelligence"},{"key":"9095_CR9","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. (2004). CP-nets: A tool for representing and reasoning with conditional ceteris paribus preference statements. Journal of Artificial Intelligence Research, 21, 135\u2013191.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"9095_CR10","doi-asserted-by":"crossref","unstructured":"Buresh-Oppenheim, J., & Pitassi, T. (2003). The complexity of resolution refinements. In Proc. LICS (pp. 138\u2013147).","DOI":"10.1109\/LICS.2003.1210053"},{"key":"9095_CR11","unstructured":"B\u00fcttner, M., & Rintanen, J. (2005). Satisfiability planning with constraints on the number of actions. In Proc. ICAPS (pp. 292\u2013299)."},{"key":"9095_CR12","unstructured":"Castell, T., Cayrol, C., Cayrol, M., & Le Berre, D. (1996). Using the Davis and Putnam procedure for an efficient computation of preferred models. In Proc. ECAI (pp. 350\u2013354)."},{"key":"9095_CR13","volume-title":"4th Multidisciplinary Workshop on Advances in Preference Handling (MPREF\u201908)","year":"2008","unstructured":"Chomicki, J., Conitzer, V., Junker, U., & Perny, P. (Eds.) (2008). 4th Multidisciplinary Workshop on Advances in Preference Handling (MPREF\u201908). Menlo Park: AAAI."},{"issue":"1","key":"9095_CR14","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1017\/S1471068407003146","volume":"8","author":"M Codish","year":"2008","unstructured":"Codish, M., Lagoon, V., & Stuckey, P. J. (2008). Logic programming with satisfiability. Theory and Practice of Logic Programming, 8(1), 121\u2013128.","journal-title":"Theory and Practice of Logic Programming"},{"key":"9095_CR15","doi-asserted-by":"crossref","unstructured":"Codish, M., Lagoon, V., & Stuckey, P. J. (2008). Telecommunications feature subscription as a partial order constraint problem. In Proc. ICLP 2008 (pp. 749\u2013753).","DOI":"10.1007\/978-3-540-89982-2_70"},{"key":"9095_CR16","doi-asserted-by":"crossref","unstructured":"Coudert, O. (1996). On solving covering problems. In Proc. DAC (pp. 197\u2013202).","DOI":"10.1145\/240518.240555"},{"issue":"7","key":"9095_CR17","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. W. (1962). A machine program for theorem proving. Communication of ACM, 5(7), 394\u2013397.","journal-title":"Communication of ACM"},{"key":"9095_CR18","doi-asserted-by":"crossref","unstructured":"De Givry, S., Larrosa, J., Meseguer, P,, & Schieux, T. (2003). Solving Max-SAT as weighted CSP. In Proc. CP (pp. 363\u2013376).","DOI":"10.1007\/978-3-540-45193-8_25"},{"key":"9095_CR19","doi-asserted-by":"crossref","unstructured":"Di Rosa, E., Giunchiglia, E., & Maratea, M. (2008). Computing all optimal solutions in satisfiability problems with preferences. In Proc. CP (pp. 603\u2013607).","DOI":"10.1007\/978-3-540-85958-1_50"},{"key":"9095_CR20","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., & Biere, A. (2005). Effective preprocessing in SAT through variable and clause elimination. In Proc. SAT (pp. 61\u201375).","DOI":"10.1007\/11499107_5"},{"key":"9095_CR21","unstructured":"E\u00e9n, N., & S\u00f6rensson, N. (2003). An extensible SAT-solver. In Proc. SAT (pp. 502\u2013518)."},{"key":"9095_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/SAT190014","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., & S\u00f6rensson, N. (2006). Translating Pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2, 1\u201326.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"5\u20136","key":"9095_CR23","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1016\/j.artint.2008.10.012","volume":"173","author":"A Gerevini","year":"2009","unstructured":"Gerevini, A., Haslum, P., Long, D., Saetti, A., & Dimopoulos, Y. (2009). Deterministic planning in the 5th IPC: PDDL3 and experimental evaluation of the planners. Artificial Intelligence, 173(5\u20136), 619\u2013668.","journal-title":"Artificial Intelligence"},{"key":"9095_CR24","unstructured":"Giunchiglia, E., & Maratea, M. (2006). Solving optimization problems with DLL. In Proc. ECAI (pp. 377\u2013381)."},{"key":"9095_CR25","unstructured":"Giunchiglia, E., & Maratea, M. (2007). Planning as satisfiability with preferences. In Proc. AAAI (pp. 987\u2013992)."},{"key":"9095_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1613\/jair.2347","volume":"31","author":"F Heras","year":"2008","unstructured":"Heras, F., Larrosa, J., & Oliveras, A. (2008). MiniMaxSat: A new weighted Max-SAT solver. Journal of Artificial Intelligence Research, 31, 1\u201332.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"9095_CR27","unstructured":"Jackson, P., & Sheridan, D. (2004). Clause form conversions for Boolean circuits. In Proc. SAT (pp. 183\u2013198)."},{"issue":"4","key":"9095_CR28","doi-asserted-by":"crossref","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. (2005). Unrestricted vs restricted cut in a tableau method for Boolean circuits. Annals of Mathematics and Artificial Intelligence, 44(4), 373\u2013399.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"9095_CR29","doi-asserted-by":"crossref","unstructured":"Jin, H., & Somenzi, F. (2005). Prime clauses for fast enumeration of satisfying assignments to boolean circuits. In Proc. DAC (pp. 750\u2013753).","DOI":"10.1145\/1065579.1065775"},{"key":"9095_CR30","unstructured":"Kautz, H., & Selman, B. (1992). Planning as satisfiability. In Proc. ECAI (pp. 359\u2013363)."},{"key":"9095_CR31","unstructured":"Larrosa, J., & Schiex, T. (2003). In the quest of the best form of local consistency for weighted CSP. In Proc. IJCAI 2003 (pp. 239\u2013244)."},{"key":"9095_CR32","unstructured":"Le Berre, D., & Simon, L. (2004). Fifty-five solvers in Vancouver: The SAT 2004 competition. In Proc. SAT (selected papers) (pp. 321\u2013344)."},{"key":"9095_CR33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/SAT190013","volume":"2","author":"D Berre Le","year":"2006","unstructured":"Le Berre, D., & Simon, L. (2006). Preface to the special volume on the SAT 2005 competitions and evaluation. Journal on Satisfiability, Boolean Modeling and Computation, 2, 1\u201314.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9095_CR34","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1613\/jair.2215","volume":"30","author":"CM Li","year":"2007","unstructured":"Li, C. M., Manya, F., & Planes, J. (2007). New inference rules for Max-SAT. Journal of Artificial Intelligence Research, 30, 321\u2013359.","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"1","key":"9095_CR35","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M. H., & Sakallah, K. A., (2008). Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning, 40(1), 1\u201333.","journal-title":"Journal of Automated Reasoning"},{"key":"9095_CR36","doi-asserted-by":"crossref","unstructured":"Manquinho, V. M., Flores, P. F., Marques Silva, J. P., & Oliveira, A. L., (1997). Prime implicant computation using satisfiability algorithms. In Proc. ICTAI (pp. 232\u2013239).","DOI":"10.1109\/TAI.1997.632261"},{"key":"9095_CR37","unstructured":"Manquinho, V. M., & Marques-Silva, J. P. (2000). On solving boolean optimization with satisfiability-based algorithms. In Proc. AMAI."},{"key":"9095_CR38","doi-asserted-by":"crossref","first-page":"209","DOI":"10.3233\/SAT190023","volume":"2","author":"VM Manquinho","year":"2006","unstructured":"Manquinho, V. M., & Marques-Silva, J. P. (2006). On using cutting planes in Pseudo-boolean optimization. Journal on Satisfiability, Boolean Modeling and Computation, 2, 209\u2013219.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9095_CR39","doi-asserted-by":"crossref","unstructured":"Manquinho, V. M., Marques Silva, J. P. & Planes, J. (2009). Algorithms for weighted boolean optimization. In Proc. SAT 2009 (pp. 495\u2013508).","DOI":"10.1007\/978-3-642-02777-2_45"},{"key":"9095_CR40","unstructured":"Marques-Silva, J., & Planes, J. (2008). Algorithms for maximum satisfiability using unsatisfiable cores. In Proc. DATE (pp. 408\u2013413)."},{"key":"9095_CR41","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J. P., & Sakallah, K. A. (1996). GRASP\u2014a new search algorithm for satisfiability. In Proc. ICCAD (pp. 220\u2013227).","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"9095_CR42","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking: An approach to the state explosion problem","author":"KL McMillan","year":"1993","unstructured":"McMillan, K. L. (1993). Symbolic model checking: An approach to the state explosion problem. Dordrecht: Kluwer Academic."},{"key":"9095_CR43","doi-asserted-by":"crossref","unstructured":"McMillan, K. L. (2002). Applying SAT methods in unbounded symbolic model checking. In Proc. CAV (pp. 250\u2013264).","DOI":"10.1007\/3-540-45657-0_19"},{"key":"9095_CR44","first-page":"112","volume":"85","author":"DG Mitchell","year":"2005","unstructured":"Mitchell, D. G. (2005). A SAT solver primer. Bulletin of the European Association for Theoretical Computer Science, 85, 112\u2013132.","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"9095_CR45","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 Proc. DAC (pp. 530\u2013535).","DOI":"10.1145\/378239.379017"},{"key":"9095_CR46","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted, D. A., & Greenbaum, S. (1986). A structure-preserving clause form translation. Journal of Symbolic Computation 2, 293\u2013304.","journal-title":"Journal of Symbolic Computation"},{"key":"9095_CR47","unstructured":"Prestwich, S. D., Rossi, F., Venable, K. B., & Walsh, T. (2005). Constraint-based preferential optimization. In Proc. AAAI (pp. 461\u2013466)."},{"key":"9095_CR48","doi-asserted-by":"crossref","unstructured":"Ramirez, M., & Geffner, H. (2007). Structural relaxations by variable renaming and their compilation for solving MinCostSAT. In Proc. CP (pp. 605\u2013619).","DOI":"10.1007\/978-3-540-74970-7_43"},{"key":"9095_CR49","doi-asserted-by":"crossref","unstructured":"Ravi, K., & Somenzi, F. (2004). Minimal assignments for bounded model checking. In Proc. TACAS (pp. 31\u201345).","DOI":"10.1007\/978-3-540-24730-2_3"},{"issue":"1\u20132","key":"9095_CR50","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/S0004-3702(00)00054-0","volume":"123","author":"C Sakama","year":"2000","unstructured":"Sakama, C., & Inoue, K. (2000). Prioritized logic programming and its application to commonsense reasoning. Artificial Intelligence, 123(1\u20132), 185\u2013222.","journal-title":"Artificial Intelligence"},{"key":"9095_CR51","doi-asserted-by":"crossref","unstructured":"Sheini, H. M., & Sakallah, K. A. (2005). Pueblo: A modern Pseudo-Boolean Sat solver. In Proc. DATE (pp. 684\u2013685).","DOI":"10.1109\/DATE.2005.246"},{"key":"9095_CR52","first-page":"1967","volume-title":"Automation of reasoning: Classical papers in computational logic (Vol. 1\u20132)","year":"1983","unstructured":"Siekmann, J., & Wrightson, G. (Eds.) (1983). Automation of reasoning: Classical papers in computational logic (Vol. 1\u20132, pp. 1967\u20131970). New York: Springer."},{"key":"9095_CR53","first-page":"466","volume":"8","author":"GS Tseitin","year":"1970","unstructured":"Tseitin, G. S. (1970). On the complexity of proofs in propositional logics. Seminars in Mathematics, 8, 466\u2013483 (Reprinted in [52]).","journal-title":"Seminars in Mathematics"},{"key":"9095_CR54","doi-asserted-by":"crossref","unstructured":"Van Nieuwenborgh, D., Heymans, S., & Vermeir, D. (2004). On programs with linearly ordered multiple preferences. In Proc. ICLP (pp. 180\u2013194).","DOI":"10.1007\/978-3-540-27775-0_13"},{"issue":"1\u20132","key":"9095_CR55","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1017\/S1471068404002315","volume":"6","author":"D Nieuwenborgh Van","year":"2006","unstructured":"Van Nieuwenborgh, D., & Vermeir, D. (2006). Preferred answer sets for ordered logic programs. Theory and Practice of Logic Programming, 6(1\u20132), 107\u2013167.","journal-title":"Theory and Practice of Logic Programming"},{"issue":"2","key":"9095_CR56","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"JP Warners","year":"1998","unstructured":"Warners, J. P. (1998). A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 68(2), 63\u201369.","journal-title":"Information Processing Letters"},{"issue":"1\u20132","key":"9095_CR57","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/j.artint.2005.01.004","volume":"164","author":"Z Xing","year":"2005","unstructured":"Xing, Z., & Zhang, W. (2005). MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability. Artificial Intelligence, 164(1\u20132), 47\u201380.","journal-title":"Artificial Intelligence"}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-010-9095-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-010-9095-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-010-9095-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,6]],"date-time":"2020-06-06T11:41:11Z","timestamp":1591443671000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-010-9095-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7,3]]},"references-count":57,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,10]]}},"alternative-id":["9095"],"URL":"https:\/\/doi.org\/10.1007\/s10601-010-9095-y","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,7,3]]}}}