{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T16:11:06Z","timestamp":1746115866501,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642415234"},{"type":"electronic","value":"9783642415241"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41524-1_18","type":"book-chapter","created":{"date-parts":[[2013,11,15]],"date-time":"2013-11-15T10:48:20Z","timestamp":1384512500000},"page":"297-304","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Coprocessor \u2013 a Standalone SAT Preprocessor"],"prefix":"10.1007","author":[{"given":"Norbert","family":"Manthey","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,11,16]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning sat solvers. In: Fox, M., Poole, D. (eds.) AAAI. AAAI Press (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (1971)","DOI":"10.1145\/800157.805047"},{"key":"18_CR3","first-page":"61","volume-title":"SAT 2005. LNCS","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)"},{"key":"18_CR4","first-page":"357","volume-title":"LPAR-17. LNCS","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. 6397, pp. 357\u2013371. Springer, Heidelberg (2010)"},{"key":"18_CR5","first-page":"201","volume-title":"SAT 2011. LNCS","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)"},{"key":"18_CR6","first-page":"340","volume-title":"SAT 2010. LNCS","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. 6175, pp. 340\u2013345. Springer, Heidelberg (2010)"},{"key":"18_CR7","first-page":"129","volume-title":"TACAS 2010. LNCS","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)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Lynce, I., Marques-Silva, J.: Probing-based preprocessing techniques for propositional satisfiability. In: ICTAI, pp. 105\u2013110. IEEE Computer Society (2003)","DOI":"10.1109\/TAI.2003.1250177"},{"key":"18_CR9","unstructured":"Manthey, N.: Solver Submission of riss 1.0 to the SAT Competition 2011. Tech. Rep. 1, Knowledge Representation and Reasoning Group, TU Dresden, Dresden, Germany (2011)"},{"key":"18_CR10","unstructured":"Manthey, N., Steinke, P.: Quadratic Direct Encoding vs. Linear Order Encoding. Tech. rep, Knowledge Representation and Reasoning Group, TU Dresden, Dresden, Germany (2011)"},{"key":"18_CR11","unstructured":"S\u00f6rensson, N.: Minisat 2.2 and minisat++ 1.1. http:\/\/baldur.iti.uka.de\/sat-race-2010\/descriptions\/solver_25+26.pdf (2010)"},{"key":"18_CR12","unstructured":"Piette, C., Hamadi, Y., Sa\u00efs, L.: Vivifying propositional clausal formulae. In: ECAI, pp. 525\u2013529. IOS Press (2008)"}],"container-title":["Lecture Notes in Computer Science","Applications of Declarative Programming and Knowledge Management"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41524-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T20:39:25Z","timestamp":1746045565000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-41524-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642415234","9783642415241"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41524-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]},"assertion":[{"value":"16 November 2013","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}