{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T09:11:50Z","timestamp":1783674710813,"version":"3.55.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319662626","type":"print"},{"value":"9783319662633","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66263-3_28","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T04:05:11Z","timestamp":1502165111000},"page":"449-456","source":"Crossref","is-referenced-by-count":8,"title":["MaxPre: An Extended MaxSAT Preprocessor"],"prefix":"10.1007","author":[{"given":"Tuukka","family":"Korhonen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jeremias","family":"Berg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Saikko","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matti","family":"J\u00e4rvisalo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"issue":"2","key":"28_CR1","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1137\/0201008","volume":"1","author":"A Aho","year":"1972","unstructured":"Aho, A., Garey, M., Ullman, J.: The transitive reduction of a directed graph. SIAM J. Comput. 1(2), 131\u2013137 (1972)","journal-title":"SIAM J. Comput."},{"issue":"2","key":"28_CR2","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/s10601-010-9105-0","volume":"16","author":"R As\u00edn","year":"2011","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195\u2013221 (2011)","journal-title":"Constraints"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Bayardo, R.J., Panda, B.: Fast algorithms for finding extremal sets. In: Proceedings of SDM, pp. 25\u201334. SIAM\/Omnipress (2011)","DOI":"10.1137\/1.9781611972818.3"},{"key":"28_CR4","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. LNCS, vol. 7795, pp. 108\u2013123. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36742-7_8"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-642-45221-5_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A Belov","year":"2013","unstructured":"Belov, A., Morgado, A., Marques-Silva, J.: SAT-based preprocessing for MaxSAT. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 96\u2013111. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-45221-5_7"},{"key":"28_CR6","unstructured":"Berg, J., Saikko, P., J\u00e4rvisalo, M.: Improving the effectiveness of SAT-based preprocessing for MaxSAT. In: Proceedings of IJCAI, pp. 239\u2013245. AAAI Press (2015)"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Berg, J., Saikko, P., J\u00e4rvisalo, M.: Re-using auxiliary variables for MaxSAT preprocessing. In: Proceedings of ICTAI, pp. 813\u2013820. IEEE Computer Society (2015)","DOI":"10.1109\/ICTAI.2015.120"},{"key":"28_CR8","unstructured":"Berg, J., Saikko, P., J\u00e4rvisalo, M.: Subsumed label elimination for maximum satisfiability. In: Proceedings of ECAI. Frontiers in Artificial Intelligence and Applications, vol. 285, pp. 630\u2013638. IOS Press (2016)"},{"issue":"1","key":"28_CR9","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/TSMCB.2002.805807","volume":"34","author":"R Brafman","year":"2004","unstructured":"Brafman, R.: A simplifier for propositional formulas with many binary clauses. IEEE Trans. Syst. Man Cybern. Part B 34(1), 52\u201359 (2004)","journal-title":"IEEE Trans. Syst. Man Cybern. Part B"},{"issue":"3","key":"28_CR10","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1287\/moor.4.3.233","volume":"4","author":"V Chvatal","year":"1979","unstructured":"Chvatal, V.: A greedy heuristic for the set-covering problem. Math. Oper. Res. 4(3), 233\u2013235 (1979)","journal-title":"Math. Oper. Res."},{"key":"28_CR11","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. 3569, pp. 61\u201375. Springer, Heidelberg (2005). doi: 10.1007\/11499107_5"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"Gimpel, J.F.: A reduction technique for prime implicant tables. In: Proceedings of SWCT, pp. 183\u2013191. IEEE Computer Society (1964)","DOI":"10.1109\/SWCT.1964.4"},{"issue":"1\/2","key":"28_CR13","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1023\/A:1006366304347","volume":"24","author":"J Groote","year":"2000","unstructured":"Groote, J., Warners, J.: The propositional formula checker HeerHugo. J. Autom. Reasoning 24(1\/2), 101\u2013125 (2000)","journal-title":"J. Autom. Reasoning"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-21581-0_17","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"MJH Heule","year":"2011","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Efficient CNF simplification based on binary implication graphs. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 201\u2013215. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21581-0_17"},{"key":"28_CR15","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. 6015, pp. 129\u2013144. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-12002-2_10"},{"key":"28_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31365-3_28"},{"key":"28_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71070-7_24"},{"key":"28_CR18","unstructured":"Li, C.: Integrating equivalency reasoning into Davis-Putnam procedure. In: Proceedings of AAAI, pp. 291\u2013296 (2000)"},{"key":"28_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-31612-8_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"N Manthey","year":"2012","unstructured":"Manthey, N.: Coprocessor 2.0 \u2013 a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 436\u2013441. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31612-8_34"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-39611-3_14","volume-title":"Hardware and Software: Verification and Testing","author":"N Manthey","year":"2013","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 102\u2013117. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39611-3_14"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Marinov, M., Nash, N., Gregg, D.: Practical algorithms for finding extremal sets. J. Exp. Algorithmics 21, Article 1.9 (2016)","DOI":"10.1145\/2893184"},{"key":"28_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/978-3-319-40970-2_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"P Saikko","year":"2016","unstructured":"Saikko, P., Berg, J., J\u00e4rvisalo, M.: LMHS: a SAT-IP hybrid MaxSAT solver. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 539\u2013546. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_34"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"Slav\u00edk, P.: A tight analysis of the greedy algorithm for set cover. In: Proceedings of STOC, pp. 435\u2013441. ACM (1996)","DOI":"10.1145\/237814.237991"},{"issue":"1","key":"28_CR24","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/s10472-005-0433-5","volume":"43","author":"A Gelder Van","year":"2005","unstructured":"Van Gelder, A.: Toward leaner binary-clause reasoning in a satisfiability solver. Ann. Math. Artif. Intell. 43(1), 239\u2013253 (2005)","journal-title":"Ann. Math. Artif. Intell."}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T23:36:11Z","timestamp":1569972971000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}