{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T17:10:08Z","timestamp":1746378608488,"version":"3.40.4"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319112053"},{"type":"electronic","value":"9783319112060"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11206-0_12","type":"book-chapter","created":{"date-parts":[[2014,9,15]],"date-time":"2014-09-15T01:31:55Z","timestamp":1410744715000},"page":"111-122","source":"Crossref","is-referenced-by-count":1,"title":["Formula Simplifications as DRAT Derivations"],"prefix":"10.1007","author":[{"given":"Norbert","family":"Manthey","sequence":"first","affiliation":[]},{"given":"Tobias","family":"Philipp","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Arnold, H.: A linearized DPLL calculus with clause learning. Tech. rep., Universit\u00e4t Potsdam. Institut f\u00fcr Informatik (2009)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-21581-0_16","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"G. Audemard","year":"2011","unstructured":"Audemard, G., Lagniez, J.-M., Mazure, B., Sa\u00efs, L.: On freezing and reactivating learnt clauses. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 188\u2013200. Springer, Heidelberg (2011)"},{"key":"12_CR3","first-page":"399","volume-title":"IJCAI 2009","author":"G. Audemard","year":"2009","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI 2009, pp. 399\u2013404. Morgan Kaufmann Publishers Inc., Pasadena (2009)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-24605-3_26","volume-title":"Theory and Applications of Satisfiability Testing","author":"F. Bacchus","year":"2004","unstructured":"Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 341\u2013355. Springer, Heidelberg (2004)"},{"issue":"1","key":"12_CR5","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligene Research\u00a022(1), 319\u2013351 (2004)","journal-title":"Journal of Artificial Intelligene Research"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: DAC 1999, pp. 317\u2013320 (1999)","DOI":"10.21236\/ADA360973"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Blum, M., Kannan, S.: Designing programs that check their work. In: Johnson, D.S. (ed.) STOC 1989, pp. 86\u201397. ACM (1989)","DOI":"10.1145\/73007.73015"},{"key":"12_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":"12_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)"},{"key":"12_CR10","unstructured":"Gelder, A.V.: Extracting (easily) checkable proofs from a satisfiability solver that employs both preorder and postorder resolution. In: ISAIM 2002 (2002)"},{"key":"12_CR11","first-page":"10886","volume-title":"DATE 2003","author":"E. Goldberg","year":"2003","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE 2003, pp. 10886\u201310891. IEEE Computer Society, Washington, DC (2003)"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-31087-4_18","volume-title":"Advanced Research in Applied Artificial Intelligence","author":"P. Gro\u00dfmann","year":"2012","unstructured":"Gro\u00dfmann, P., H\u00f6lldobler, S., Manthey, N., Nachtigall, K., Opitz, J., Steinke, P.: Solving periodic event scheduling problems with SAT. In: Jiang, H., Ding, W., Ali, M., Wu, X. (eds.) IEA\/AIE 2012. LNCS, vol.\u00a07345, pp. 166\u2013175. Springer, Heidelberg (2012)"},{"key":"12_CR13","first-page":"499","volume-title":"IJCAI 2009","author":"Y. Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Control-based clause sharing in parallel SAT solving. In: Boutilier, C. (ed.) IJCAI 2009, pp. 499\u2013504. Morgan Kaufmann Publishers Inc., Pasadena (2009)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-02777-2_21","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"H. Han","year":"2009","unstructured":"Han, H., Somenzi, F.: On-the-fly clause improvement. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 209\u2013222. Springer, Heidelberg (2009)"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Heule, M., Hunt Jr., W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Jobstman, B., Ray, S. (eds.) FMCAD 2013, pp. 181\u2013188. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-38574-2_24","volume-title":"Automated Deduction \u2013 CADE-24","author":"M.J.H. Heule","year":"2013","unstructured":"Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 345\u2013359. Springer, Heidelberg (2013)"},{"key":"12_CR17","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)"},{"key":"12_CR18","unstructured":"Heule, M., J\u00e4rvisalo, M., Biere, A.: Covered clause elimination. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR\u00a02010. LNCS, vol. 6397, pp. 41\u201346. Springer, Heidelberg (2010)"},{"key":"12_CR19","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)"},{"key":"12_CR20","unstructured":"H\u00f6lldobler, S., Manthey, N., Philipp, T., Steinke, P.: Generic CDCL \u2013 A formalization of modern propositional satisfiability solvers. In: POS 2014 (accepted, 2014)"},{"key":"12_CR21","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":"12_CR22","series-title":"Lecture Notes in Computer Science","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, vol.\u00a07364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-20662-7_23","volume-title":"Experimental Algorithms","author":"M. Kaufmann","year":"2011","unstructured":"Kaufmann, M., Kottler, S.: Beyond unit propagation in SAT solving. In: Pardalos, P.M., Rebennack, S. (eds.) SEA 2011. LNCS, vol.\u00a06630, pp. 267\u2013279. Springer, Heidelberg (2011)"},{"key":"12_CR24","first-page":"359","volume-title":"ECAI 1992","author":"H. Kautz","year":"1992","unstructured":"Kautz, H., Selman, B.: Planning as satisfiability. In: Neumann, B. (ed.) ECAI 1992, pp. 359\u2013363. John Wiley & Sons, Inc., New York (1992)"},{"key":"12_CR25","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":"12_CR26","first-page":"291","volume-title":"IAAI 2000","author":"C.M. Li","year":"2000","unstructured":"Li, C.M.: Integrating equivalency reasoning into davis-putnam procedure. In: Kautz, H.A., Porter, B.W. (eds.) IAAI 2000, pp. 291\u2013296. AAAI Press, Menlo Park (2000)"},{"key":"12_CR27","first-page":"104","volume-title":"AAAI 2006","author":"I. Lynce","year":"2006","unstructured":"Lynce, I., Marques-Silva, J.: Efficient haplotype inference with Boolean satisfiability. In: AAAI 2006, pp. 104\u2013109. AAAI Press, Menlo Park (2006)"},{"key":"12_CR28","first-page":"105","volume-title":"ICTAI 2003","author":"I. Lynce","year":"2003","unstructured":"Lynce, I., Marques-Silva, J.P.: Probing-based preprocessing techniques for propositional satisfiability. In: ICTAI 2003, pp. 105\u2013110. IEEE Computer Society, Sacramento (2003)"},{"key":"12_CR29","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. LNCS, vol.\u00a07857, pp. 102\u2013117. Springer, Heidelberg (2013)"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-39071-5_4","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"N. Manthey","year":"2013","unstructured":"Manthey, N., Philipp, T., Wernhard, C.: Soundness of inprocessing in clause sharing SAT\u00a0solvers. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 22\u201339. Springer, Heidelberg (2013)"},{"issue":"1","key":"12_CR31","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/s10817-009-9127-8","volume":"43","author":"F. Mari\u0107","year":"2009","unstructured":"Mari\u0107, F.: Formalization and implementation of modern SAT solvers. Journal of Automated Reasoning\u00a043(1), 81\u2013119 (2009)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"12_CR32","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"R.M. McConnell","year":"2011","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Computer Science Review\u00a05(2), 119\u2013161 (2011)","journal-title":"Computer Science Review"},{"key":"12_CR33","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-540-32275-7_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 36\u201350. Springer, Heidelberg (2005)"},{"key":"12_CR34","unstructured":"Piette, C., Hamadi, Y., Sais, L.: Vivifying propositional clausal formulae. In: Ghallab, M., Spyropoulos, C.D., Fakotakis, N., Avouris, N.M. (eds.) ECAI 2008, pp. 525\u2013529. IOS Press (2008)"},{"key":"12_CR35","doi-asserted-by":"crossref","unstructured":"Rintanen, J.: Engineering efficient planners with SAT. In: Raedt, L.D., Bessi\u00e8re, C., Dubois, D., Doherty, P., Frasconi, P., Heintz, F., Lucas, P.J.F. (eds.) ECAI 2012. Frontiers in Artificial Intelligence and Applications, vol. 242, pp. 684\u2013689. IOS Press (2012)","DOI":"10.3233\/978-1-61499-098-7-684"},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/11527695_22","volume-title":"Theory and Applications of Satisfiability Testing","author":"S. Subbarayan","year":"2005","unstructured":"Subbarayan, S., Pradhan, D.K.: NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 276\u2013291. Springer, Heidelberg (2005)"},{"key":"12_CR37","series-title":"Symbolic Computation","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning","author":"G.S. Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation, pp. 466\u2013483. Springer, Heidelberg (1983)"},{"key":"12_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-39634-2_18","volume-title":"Interactive Theorem Proving","author":"N. Wetzler","year":"2013","unstructured":"Wetzler, N., Heule, M.J.H., Hunt Jr., W.A.: Mechanical verification of SAT refutations with extended resolution. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 229\u2013244. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","KI 2014: Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11206-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T16:32:50Z","timestamp":1746376370000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-11206-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319112053","9783319112060"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11206-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}