{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T11:59:54Z","timestamp":1792756794299,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642313646","type":"print"},{"value":"9783642313653","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31365-3_28","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T20:35:34Z","timestamp":1340310934000},"page":"355-370","source":"Crossref","is-referenced-by-count":117,"title":["Inprocessing Rules"],"prefix":"10.1007","author":[{"given":"Matti","family":"J\u00e4rvisalo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"5","key":"28_CR1","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Computers"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proc. DAC, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"28_CR3","unstructured":"Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: Proc. AAAI, pp. 613\u2013619. AAAI Press (2002)"},{"key":"28_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)"},{"key":"28_CR5","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: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 276\u2013291. Springer, Heidelberg (2005)"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/11499107_34","volume-title":"Theory and Applications of Satisfiability Testing","author":"R. Gershman","year":"2005","unstructured":"Gershman, R., Strichman, O.: Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 423\u2013429. Springer, Heidelberg (2005)"},{"key":"28_CR7","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)"},{"issue":"2","key":"28_CR8","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.entcs.2004.06.062","volume":"119","author":"H. Jin","year":"2005","unstructured":"Jin, H., Somenzi, F.: An incremental algorithm to check satisfiability for bounded model checking. Electronic Notes in Theoretical Computer Science\u00a0119(2), 51\u201365 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Han, H., Somenzi, F.: Alembic: An efficient algorithm for CNF preprocessing. In: Proc. DAC, pp. 582\u2013587. IEEE (2007)","DOI":"10.1145\/1278480.1278628"},{"key":"28_CR10","unstructured":"Piette, C., Hamadi, Y., Sa\u00efs, L.: Vivifying propositional clausal formulae. In: Proc. ECAI, pp. 525\u2013529. IOS Press (2008)"},{"key":"28_CR11","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.J.H. Heule","year":"2010","unstructured":"Heule, M.J.H., 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":"28_CR12","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Simulating circuit-level simplifications on CNF. Journal of Automated Reasoning (2012); OnlineFirst 2011","DOI":"10.1007\/s10817-011-9239-9"},{"key":"28_CR13","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":"28_CR14","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Covered clause elimination. In: LPAR-17 Short Papers (2010), http:\/\/arxiv.org\/abs\/1011.5202"},{"key":"28_CR15","unstructured":"Biere, A.: P{re,i}coSAT@SC 2009. In: SAT 2009 Competitive Event Booklet (2009)"},{"key":"28_CR16","unstructured":"Soos, M.: CryptoMiniSat 2.5.0, SAT Race 2010 solver description (2010)"},{"key":"28_CR17","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Technical Report 10\/1, Johannes Kepler University, Linz, Austria (2010)"},{"key":"28_CR18","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)"},{"issue":"6","key":"28_CR19","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814948_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A.: On SAT Modulo Theories and Optimization Problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 156\u2013169. Springer, Heidelberg (2006)"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Larrosa, J., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: A framework for certified boolean branch-and-bound optimization. Journal of Automated Reasoning 46(1) (2011)","DOI":"10.1007\/s10817-010-9176-z"},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"Andersson, G., Bjesse, P., Cook, B., Hanna, Z.: A proof engine approach to solving combinational design automation problems. In: Proc.\u00a0DAC, pp. 725\u2013730. ACM (2002)","DOI":"10.1145\/514100.514101"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning 2, pp. 466\u2013483. Springer (1983)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"28_CR24","unstructured":"Li, C.M.: Integrating equivalency reasoning into Davis-Putnam procedure. In: Proc. AAAI, pp. 291\u2013296. AAAI Press (2000)"},{"key":"28_CR25","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res.\u00a022, 319\u2013351 (2004)","journal-title":"J. Artif. Intell. Res."},{"key":"28_CR26","doi-asserted-by":"crossref","unstructured":"Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning SAT solvers. In: Proc. AAAI. AAAI Press (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"issue":"15","key":"28_CR27","doi-asserted-by":"publisher","first-page":"1277","DOI":"10.1016\/j.artint.2010.07.008","volume":"174","author":"J. Huang","year":"2010","unstructured":"Huang, J.: Extended clause learning. Artificial Intelligence\u00a0174(15), 1277\u20131284 (2010)","journal-title":"Artificial Intelligence"},{"key":"28_CR28","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":"28_CR29","doi-asserted-by":"crossref","unstructured":"Hamadi, Y., Jabbour, S., Sa\u00efs, L.: Learning for dynamic subsumption. In: Proc. ICTAI, pp. 328\u2013335. IEEE (2009)","DOI":"10.1109\/ICTAI.2009.22"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31365-3_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T20:46:26Z","timestamp":1687553186000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31365-3_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313646","9783642313653"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}