{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T11:59:48Z","timestamp":1792756788023,"version":"4.5.0"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2011,11,3]],"date-time":"2011-11-03T00:00:00Z","timestamp":1320278400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,12]]},"DOI":"10.1007\/s10817-011-9239-9","type":"journal-article","created":{"date-parts":[[2011,11,2]],"date-time":"2011-11-02T17:47:26Z","timestamp":1320256046000},"page":"583-619","source":"Crossref","is-referenced-by-count":35,"title":["Simulating Circuit-Level Simplifications on CNF"],"prefix":"10.1007","volume":"49","author":[{"given":"Matti","family":"J\u00e4rvisalo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2011,11,3]]},"reference":[{"key":"9239_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.) Proceedings of the 24th AAAI Conference on Artificial Intelligence (AAAI 2010). AAAI Press (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"9239_CR2","unstructured":"Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: Proceedings of the 18th National Conference on Artificial Intelligence (AAAI 2002), pp. 613\u2013619. AAAI Press (2002)"},{"key":"9239_CR3","doi-asserted-by":"crossref","unstructured":"Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. In: Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003). Lecture Notes in Computer Science, vol. 2919, pp. 341\u2013355. Springer (2004)","DOI":"10.1007\/978-3-540-24605-3_26"},{"key":"9239_CR4","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., et al. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825\u2013885. IOS Press"},{"key":"9239_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Clarke, E.M., Raimi, R., Zhu, Y.: Verifiying safety properties of a power PC microprocessor using symbolic model checking without BDDs. In: Halbwachs, N., Peled, D., (eds.) Proceedings of the 11th International Conference on Computer Aided Verification (CAV 1999). Lecture Notes in Computer Science, vol. 1633, pp. 60\u201371. Springer (1999)","DOI":"10.1007\/3-540-48683-6_8"},{"key":"9239_CR6","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)"},{"key":"9239_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Quantified blocked clause elimination. In: Proceedings of the 23nd International Conference on Automated Deduction (CADE-23). Lecture Notes in Computer Science. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_10"},{"issue":"4","key":"9239_CR8","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1016\/0747-7171(92)90009-S","volume":"14","author":"T Boy de la Tour","year":"1992","unstructured":"Boy de la Tour, T.: An optimality result for clause form translation. J. Symb. Comput. 14(4), 283\u2013302 (1992)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"9239_CR9","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/TSMCB.2002.805807","volume":"34","author":"RI Brafman","year":"2004","unstructured":"Brafman, R.I.: 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"},{"key":"9239_CR10","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009). Lecture Notes in Computer Science, vol. 5505, pp. 174\u2013177. Springer (2009)","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"9239_CR11","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT solver. In: Gupta, A., Malik, S. (eds.) Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008). Lecture Notes in Computer Science, vol. 5123, pp. 299\u2013303. Springer (2008)","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"9239_CR12","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT solver. In: Esparza, J., Majumdar, R. (eds.) Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010). Lecture Notes in Computer Science, vol. 6015, pp. 150\u2013153. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"9239_CR13","doi-asserted-by":"crossref","unstructured":"Chambers, B., Manolios, P., Vroon, D.: Faster SAT solving with better CNF generation. In: Proceedings of Design, Automation and Test in Europe (DATE 2009), pp. 1590\u20131595. IEEE (2009)","DOI":"10.1109\/DATE.2009.5090918"},{"issue":"3","key":"9239_CR14","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"9239_CR15","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9239_CR16","doi-asserted-by":"crossref","unstructured":"Drechsler, R., Junttila, T., Niemel\u00e4, I.: Non-clausal SAT and ATPG. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, chap. 21, pp. 655\u2013694. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-655"},{"key":"9239_CR17","unstructured":"Dunham, B., Fridshal, R., Sward, G.: A heuristic program for proving elementary logical theorems. In: Proceedings of the International Conference on Information Processing (IFIP 1959), pp. 282\u2013284 (1959)"},{"key":"9239_CR18","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0003-4843(76)90020-6","volume":"10","author":"B Dunham","year":"1976","unstructured":"Dunham, B., Wang, H.: Towards feasible solutions of the tautology problem. Ann. Math. Logic 10, 117\u2013154 (1976)","journal-title":"Ann. Math. Logic"},{"key":"9239_CR19","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) Proceedings of 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005). Lecture Notes in Computer Science, vol. 3569, pp. 61\u201375. Springer (2005)","DOI":"10.1007\/11499107_5"},{"key":"9239_CR20","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., Mishchenko, A., S\u00f6rensson, N.: Applying logic synthesis for speeding up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007). Lecture Notes in Computer Science, vol. 4501, pp. 272\u2013286. Springer (2007)","DOI":"10.1007\/978-3-540-72788-0_26"},{"key":"9239_CR21","doi-asserted-by":"crossref","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007). Lecture Notes in Computer Science, vol. 4590, pp. 519\u2013531. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"9239_CR22","doi-asserted-by":"crossref","unstructured":"Gershman, R., Strichman, O.: Cost-effective hyper-resolution for preprocessing CNF formulas. In: Bacchus, F., Walsh, T. (eds.) Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005). Lecture Notes in Computer Science, vol. 3569, pp. 423\u2013429. Springer (2005)","DOI":"10.1007\/11499107_34"},{"key":"9239_CR23","doi-asserted-by":"crossref","unstructured":"Han, H., Somenzi, F.: Alembic: an efficient algorithm for CNF preprocessing. In: Proceedings of the 44rd Design Automation Conference (DAC 2007), pp. 582\u2013587 (2007)","DOI":"10.1109\/DAC.2007.375231"},{"key":"9239_CR24","doi-asserted-by":"crossref","unstructured":"Han, H., Somenzi, F.: On-the-fly clause improvement. In: Kullmann, O. (ed.) SAT. Lecture Notes in Computer Science, vol. 5584, pp. 209\u2013222. Springer (2009)","DOI":"10.1007\/978-3-642-02777-2_21"},{"key":"9239_CR25","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., van Maaren, H.: Aligning CNF- and equivalence-reasoning. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2005 Selected Revised Papers. Lecture Notes in Computer Science, vol. 3542, pp. 145\u2013156. Springer (2005)","DOI":"10.1007\/11527695_12"},{"key":"9239_CR26","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Verwer, S.: Exact DFA identification using SAT solvers. In: Sempere, J.M., Garc\u00eda, P. (eds.) Proceedings of the 10th International Colloquium on Grammatical Inference: Theoretical Results and Applications (ICGI 2010). Lecture Notes in Computer Science, vol. 6339, pp. 66\u201379 (2010)","DOI":"10.1007\/978-3-642-15488-1_7"},{"issue":"15","key":"9239_CR27","doi-asserted-by":"crossref","first-page":"1277","DOI":"10.1016\/j.artint.2010.07.008","volume":"174","author":"J Huang","year":"2010","unstructured":"Huang, J.: Extended clause learning. Artif. Intell. 174(15), 1277\u20131284 (2010)","journal-title":"Artif. Intell."},{"key":"9239_CR28","doi-asserted-by":"crossref","unstructured":"Jackson, P., Sheridan, D.: Clause form conversions for Boolean circuits. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004 Selected Revised Papers. Lecture Notes in Computer Science, vol. 3542, pp. 183\u2013198. Springer (2005)","DOI":"10.1007\/11527695_15"},{"key":"9239_CR29","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Biere, A.: Reconstructing solutions after blocked clause elimination. In: Strichman, O., Szeider, S. (eds.) Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010). Lecture Notes in Computer Science, vol. 6175, pp. 340\u2013345. Springer (2010)","DOI":"10.1007\/978-3-642-14186-7_30"},{"key":"9239_CR30","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010). Lecture Notes in Computer Science, vol. 6015, pp. 129\u2013144. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"9239_CR31","doi-asserted-by":"crossref","unstructured":"Jha, S., Limaye, R., Seshia, S.A.: Beaver: Engineering an efficient SMT solver for bit-vector arithmetic. In: Bouajjani, A., Maler, O. (eds.) Proceedings of the 21st International Conference on Computer Aided Verification (CAV 2009). Lecture Notes in Computer Science, vol. 5643, pp. 668\u2013674. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_53"},{"issue":"2","key":"9239_CR32","doi-asserted-by":"crossref","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 119(2), 51\u201365 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"3","key":"9239_CR33","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/j.entcs.2006.12.022","volume":"174","author":"T Jussila","year":"2007","unstructured":"Jussila, T., Biere, A.: Compressing BMC encodings with QBF. Electronic Notes in Theoretical Computer Science 174(3), 45\u201356 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9239_CR34","unstructured":"Kautz, H.A., Ruan, Y., Achlioptas, D., Gomes, C.P., Selman, B., Stickel, M.E.: Balance and filtering in structured satisfiable problems. In: Nebel, B. (ed.) Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI 2001), pp. 351\u2013358. Morgan Kaufmann (2001)"},{"issue":"1\u20132","key":"9239_CR35","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(98)00017-6","volume":"223","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: New methods for 3-SAT decision and worst-case analysis. Theor. Comp. Sci. 223(1\u20132), 1\u201372 (1999)","journal-title":"Theor. Comp. Sci."},{"key":"9239_CR36","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discrete Appl. Math."},{"key":"9239_CR37","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/S1571-0653(04)00314-2","volume":"9","author":"D Le Berre","year":"2001","unstructured":"Le Berre, D.: Exploiting the real power of unit propagation lookahead. Electronic Notes in Discrete Mathematics 9, 59\u201380 (2001)","journal-title":"Electronic Notes in Discrete Mathematics"},{"key":"9239_CR38","doi-asserted-by":"crossref","unstructured":"Li, C.M., Wei, W., Zhang, H.: Combining adaptive noise and look-ahead in local search for SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007). Lecture Notes in Computer Science, pp. 121\u2013133. Springer (2007)","DOI":"10.1007\/978-3-540-72788-0_15"},{"key":"9239_CR39","unstructured":"Lynce, I., Marques-Silva, J.: The interaction between simplification and search in propositional satisfiability. In: CP\u201901 Workshop on Modeling and Problem Formulation (2001)"},{"key":"9239_CR40","doi-asserted-by":"crossref","unstructured":"Manolios, P., Vroon, D.: Efficient circuit to CNF conversion. In: Marques-Silva, J., Sakallah, K.A. (eds.) Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007). Lecture Notes in Computer Science, vol. 4501, pp. 4\u20139. Springer (2007)","DOI":"10.1007\/978-3-540-72788-0_3"},{"key":"9239_CR41","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K.: DAG-aware AIG rewriting: a fresh look at combinational logic synthesis. In: Sentovich, E. (ed.) Proceedings of the 43rd Design Automation Conference (DAC 2006), pp. 532\u2013535. ACM (2006)","DOI":"10.1109\/DAC.2006.229287"},{"key":"9239_CR42","doi-asserted-by":"crossref","unstructured":"Ostrowski, R., Gr\u00e9goire, \u00c9., Mazure, B., Sais, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Hentenryck, P.V. (ed.) Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming (CP 2002). Lecture Notes in Computer Science, vol. 2470, pp. 185\u2013199. Springer (2002)","DOI":"10.1007\/3-540-46135-3_13"},{"issue":"3","key":"9239_CR43","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293\u2013304 (1986)","journal-title":"J. Symb. Comput."},{"issue":"4","key":"9239_CR44","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1109\/TPAMI.1984.4767555","volume":"6","author":"PW Purdom","year":"1984","unstructured":"Purdom, P.W.: Solving satisfiability with less searching. IEEE Trans. Pattern Anal. Mach. Intell. 6(4), 510\u2013513 (1984)","journal-title":"IEEE Trans. Pattern Anal. Mach. Intell."},{"key":"9239_CR45","doi-asserted-by":"crossref","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 Selected Revised Papers. Lecture Notes in Computer Science, vol. 3542, pp. 276\u2013291. Springer (2005)","DOI":"10.1007\/11527695_22"},{"key":"9239_CR46","doi-asserted-by":"crossref","unstructured":"Tompkins, D.A., Hoos, H.H.: UBCSAT: an implementation and experimentation environment for SLS algorithms for SAT & MAX-SAT. In: Online Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004) (2004)","DOI":"10.1007\/11527695_24"},{"key":"9239_CR47","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 2: Classical Papers on Computational Logic 1967\u20131970, pp. 466\u2013483. Springer (1983)","DOI":"10.1007\/978-3-642-81955-1_28"},{"issue":"1","key":"9239_CR48","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":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9239-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-011-9239-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9239-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,13]],"date-time":"2025-03-13T18:30:45Z","timestamp":1741890645000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-011-9239-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11,3]]},"references-count":48,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,12]]}},"alternative-id":["9239"],"URL":"https:\/\/doi.org\/10.1007\/s10817-011-9239-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,11,3]]}}}