{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T02:19:38Z","timestamp":1725761978556},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642452208"},{"type":"electronic","value":"9783642452215"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45221-5_7","type":"book-chapter","created":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T04:28:23Z","timestamp":1386217703000},"page":"96-111","source":"Crossref","is-referenced-by-count":12,"title":["SAT-Based Preprocessing for MaxSAT"],"prefix":"10.1007","author":[{"given":"Anton","family":"Belov","sequence":"first","affiliation":[]},{"given":"Ant\u00f3nio","family":"Morgado","sequence":"additional","affiliation":[]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-02777-2_39","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"C. Ans\u00f3tegui","year":"2009","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial maxsat through satisfiability testing. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 427\u2013440. Springer, Heidelberg (2009)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-36742-7_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Belov","year":"2013","unstructured":"Belov, A., J\u00e4rvisalo, M., Marques-Silva, J.: Formula preprocessing in MUS extraction. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 108\u2013123. Springer, Heidelberg (2013)"},{"key":"7_CR3","unstructured":"Belov, A., Marques-Silva, J.: Generalizing redundancy in propositional logic: Foundations and hitting sets duality. CoRR, abs\/1207.1257 (2012)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Belov, A., Morgado, A., Marques-Silva, J.: SAT-based preprocessing for MaxSAT (extended version). CoRR, abs\/1310.2298 (2013)","DOI":"10.1007\/978-3-642-45221-5_7"},{"issue":"2-4","key":"7_CR5","first-page":"75","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. JSAT\u00a04(2-4), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"7_CR6","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Report Series Technical Report 10\/1, Johannes Kepler University, Linz, Austria (2010)"},{"issue":"8-9","key":"7_CR7","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1016\/j.artint.2007.03.001","volume":"171","author":"M.L. Bonet","year":"2007","unstructured":"Bonet, M.L., Levy, J., Many\u00e0, F.: Resolution for Max-SAT. Artif. Intell.\u00a0171(8-9), 606\u2013618 (2007)","journal-title":"Artif. Intell."},{"key":"7_CR8","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":"7_CR9","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","key":"7_CR10","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N. E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci.\u00a089(4), 543\u2013560 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11814948_25","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"Z. Fu","year":"2006","unstructured":"Fu, Z., Malik, S.: On solving the partial max-sat problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 252\u2013265. Springer, Heidelberg (2006)"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Heule, M., J\u00e4rvisalo, M., Biere, A.: Covered clause elimination. In: LPAR Short Paper (2010)","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-642-14186-7_30","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"M. J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A.: Reconstructing solutions after blocked clause elimination. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 340\u2013345. Springer, Heidelberg (2010)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-12002-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 129\u2013144. Springer, Heidelberg (2010)"},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96-97","author":"O. Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics\u00a096-97, 149\u2013176 (1999)","journal-title":"Discrete Applied Mathematics"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/11814948_4","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"O. Kullmann","year":"2006","unstructured":"Kullmann, O., Lynce, I., Marques-Silva, J.: Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 22\u201335. Springer, Heidelberg (2006)"},{"key":"7_CR17","unstructured":"Li, C.M., Manya, F.: MaxSAT, hard and soft constraints. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 613\u2013631. IOS Press (2009)"},{"key":"7_CR18","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":"7_CR19","doi-asserted-by":"crossref","unstructured":"Morgado, A., Heras, F., Liffiton, M., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints (2013)","DOI":"10.1007\/s10601-013-9146-2"},{"issue":"1","key":"7_CR20","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R. Reiter","year":"1987","unstructured":"Reiter, R.: A theory of diagnosis from first principles. Artif. Intell.\u00a032(1), 57\u201395 (1987)","journal-title":"Artif. Intell."}],"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\/978-3-642-45221-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T00:35:52Z","timestamp":1558744552000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45221-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642452208","9783642452215"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45221-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}