{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:25:32Z","timestamp":1766136332932},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642316111"},{"type":"electronic","value":"9783642316128"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31612-8_34","type":"book-chapter","created":{"date-parts":[[2012,6,18]],"date-time":"2012-06-18T09:14:42Z","timestamp":1340010882000},"page":"436-441","source":"Crossref","is-referenced-by-count":27,"title":["Coprocessor 2.0 \u2013 A Flexible CNF Simplifier"],"prefix":"10.1007","author":[{"given":"Norbert","family":"Manthey","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","unstructured":"Manthey, N.: Coprocessor \u2013 a Standalone SAT Preprocessor. In: Proceedings of the 25th Workshop on Logic Programming, WLP 2011, Infsys Research Report 1843-11-06, Technische Universit\u00e4t Wien, 99\u2013104 (2011)"},{"key":"34_CR2","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":"34_CR3","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":"34_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-16242-8_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Heule","year":"2010","unstructured":"Heule, M., J\u00e4rvisalo, M., Biere, A.: Clause Elimination Procedures for CNF Formulas. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 357\u2013371. Springer, Heidelberg (2010)"},{"issue":"2-3","key":"34_CR5","first-page":"56","volume":"7","author":"D.L. Berre","year":"2010","unstructured":"Berre, D.L., Parrain, A.: The Sat4j library, release 2.2. JSAT\u00a07(2-3), 56\u201359 (2010)","journal-title":"JSAT"},{"issue":"4","key":"34_CR6","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":"34_CR7","unstructured":"Lynce, I., Marques-Silva, J.: Probing-Based Preprocessing Techniques for Propositional Satisfiability. In: Proceedings of the 15th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2003. IEEE Computer Society (2003)"},{"key":"34_CR8","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/S0020-0190(99)00088-5","volume":"71","author":"C.M. Li","year":"1999","unstructured":"Li, C.M.: A constraint-based approach to narrow search trees for satisfiability. Inf. Process. Lett.\u00a071, 75\u201380 (1999)","journal-title":"Inf. Process. Lett."},{"key":"34_CR9","unstructured":"Piette, C., Hamadi, Y., Sa\u00efs, L.: Vivifying propositional clausal formulae. In: 18th European Conference on Artificial Intelligence (ECAI 2008), Patras, Greece, pp. 525\u2013529 (2008)"},{"key":"34_CR10","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":"M.J.H. 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.\u00a06695, pp. 201\u2013215. Springer, Heidelberg (2011)"},{"issue":"1","key":"34_CR11","doi-asserted-by":"publisher","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.\u00a043(1), 239\u2013253 (2005)","journal-title":"Ann. Math. Artif. Intell."},{"key":"34_CR12","unstructured":"Manthey, N., Steinke, P.: Quadratic Direct Encoding vs. Linear Order Encoding. Technical Report\u00a03, Knowledge Representation and Reasoning Group, Technische Universit\u00e4t Dresden, 01062 Dresden, Germany (2011)"},{"key":"34_CR13","unstructured":"Chen, J.: A New SAT Encoding of the At-Most-One Constraint. In: Proceedings of ModRef 2011 (2011)"},{"key":"34_CR14","unstructured":"Wernhard, C.: Computing with Logic as Operator Elimination: The ToyElim System. In: Proceedings of the 25th Workshop on Logic Programming, WLP 2011, Infsys Research Report 1843-11-06, Technische Universit\u00e4t Wien, pp. 94\u201398 (2011)"},{"key":"34_CR15","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report 10\/1, Institute for Formal Models and Verification, Johannes Kepler University (2010)"},{"key":"34_CR16","unstructured":"Soos, M.: CryptoMiniSat 2.5.0. In: SAT Race Competitive Event Booklet (2010)"},{"key":"34_CR17","unstructured":"Manthey, N.: Solver Description of riss and priss. Technical Report\u00a02, Knowledge Representation and Reasoning Group, Technische Universit\u00e4t Dresden, 01062 Dresden, Germany (2012)"},{"key":"34_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1670412.1670413","volume-title":"Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, SMT 2009","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Fuzzing and delta-debugging smt solvers. In: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, SMT 2009, pp. 1\u20135. ACM, New York (2009)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2012"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31612-8_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:40:18Z","timestamp":1620128418000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31612-8_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642316111","9783642316128"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31612-8_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}