{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T18:09:48Z","timestamp":1776881388638,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":48,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642396106","type":"print"},{"value":"9783642396113","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39611-3_14","type":"book-chapter","created":{"date-parts":[[2013,7,3]],"date-time":"2013-07-03T18:33:07Z","timestamp":1372876387000},"page":"102-117","source":"Crossref","is-referenced-by-count":38,"title":["Automated Reencoding of Boolean Formulas"],"prefix":"10.1007","author":[{"given":"Norbert","family":"Manthey","sequence":"first","affiliation":[]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Goldberg, E.I., Prasad, M.R., Brayton, R.K.: Using SAT for combinational equivalence checking. In: DATE, pp. 114\u2013121 (2001)"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K., E\u00e9n, N.: Improvements to combinational equivalence checking. In: Hassoun, S. (ed.) ICCAD, pp. 836\u2013843. ACM (2006)","DOI":"10.1109\/ICCAD.2006.320087"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Baumgartner, J., Mony, H., Paruthi, V., Kanzelman, R., Janssen, G.: Scalable sequential equivalence checking across arbitrary design transformations. In: ICCD. IEEE (2006)","DOI":"10.1109\/ICCD.2006.4380826"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Kaiss, D., Skaba, M., Hanna, Z., Khasidashvili, Z.: Industrial strength SAT-based alignability algorithm for hardware equivalence verification. In: FMCAD, pp. 20\u201326. IEEE Computer Society (2007)","DOI":"10.1109\/FAMCAD.2007.37"},{"key":"14_CR5","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, pp. 317\u2013320 (1999)","DOI":"10.21236\/ADA360973"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt Jr., W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"issue":"11","key":"14_CR7","doi-asserted-by":"publisher","first-page":"1804","DOI":"10.1109\/TCAD.2010.2061270","volume":"29","author":"Y. Chen","year":"2010","unstructured":"Chen, Y., Safarpour, S., Marques-Silva, J.P., Veneris, A.G.: Automated design debugging with maximum satisfiability. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a029(11), 1804\u20131817 (2010)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"issue":"5","key":"14_CR8","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":"14_CR9","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K.: Dag-aware aig rewriting a fresh look at combinational logic synthesis. In: DAC, pp. 532\u2013535 (2006)","DOI":"10.1109\/DAC.2006.229287"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-72788-0_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"N. E\u00e9n","year":"2007","unstructured":"E\u00e9n, N., Mishchenko, A., S\u00f6rensson, N.: Applying logic synthesis for speeding up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 272\u2013286. Springer, Heidelberg (2007)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Chambers, B., Manolios, P., Vroon, D.: Faster SAT solving with better CNF generation. In: DATE, pp. 1590\u20131595. IEEE (2009)","DOI":"10.1109\/DATE.2009.5090918"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Guerra e Silva, L., Miguel Silveira, L., Marques Silva, J.P.: Algorithms for solving boolean satisfiability in combinational circuits. In: DATE, pp. 526\u2013530. IEEE Computer Society (1999)","DOI":"10.1145\/307418.307557"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Ashar, P., Gupta, A., Zhang, L., Malik, S.: Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. In: DAC, pp. 747\u2013750. ACM (2002)","DOI":"10.1145\/513918.514105"},{"key":"14_CR15","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-4","key":"14_CR16","first-page":"1","volume":"2","author":"N. E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. JSAT\u00a02(1-4), 1\u201326 (2006)","journal-title":"JSAT"},{"key":"14_CR17","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":"14_CR18","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Report Series Technical Report 10\/1, Johannes Kepler University, Linz, Austria (2010)"},{"key":"14_CR19","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":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Biere","year":"2005","unstructured":"Biere, A.: Resolve and expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"14_CR21","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":"14_CR22","first-page":"731","volume-title":"DAC 2002","author":"F.A. Aloul","year":"2002","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult SAT instances in the presence of symmetry. In: DAC 2002, pp. 731\u2013736. ACM, New York (2002)"},{"issue":"3","key":"14_CR23","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1109\/TCAD.2004.842808","volume":"24","author":"D. Chai","year":"2005","unstructured":"Chai, D., Kuehlmann, A.: A fast pseudo-boolean constraint solver. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a024(3), 305\u2013317 (2005)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Planes, J.: Algorithms for maximum satisfiability using unsatisfiable cores. In: DATE, pp. 408\u2013413. IEEE (2008)","DOI":"10.1145\/1403375.1403474"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"542","DOI":"10.1007\/978-3-540-30201-8_40","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"C.-G. Quimper","year":"2004","unstructured":"Quimper, C.-G., L\u00f3pez-Ortiz, A., van Beek, P., Golynski, A.: Improved algorithms for the global cardinality constraint. In: Wallace, M. (ed.) CP 2004. LNCS, vol.\u00a03258, pp. 542\u2013556. Springer, Heidelberg (2004)"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1007\/11564751_70","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C.-G. Quimper","year":"2005","unstructured":"Quimper, C.-G., Walsh, T.: Beyond finite domains: The all different and global cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 812\u2013816. Springer, Heidelberg (2005)"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-540-72397-4_26","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"A. Zanarini","year":"2007","unstructured":"Zanarini, A., Pesant, G.: Generalizations of the global cardinality constraint for hierarchical resources. In: Van Hentenryck, P., Wolsey, L.A. (eds.) CPAIOR 2007. LNCS, vol.\u00a04510, pp. 361\u2013375. Springer, Heidelberg (2007)"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/11493853_22","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"J.-C. R\u00e9gin","year":"2005","unstructured":"R\u00e9gin, J.-C.: Combination of among and cardinality constraints. In: Bart\u00e1k, R., Milano, M. (eds.) CPAIOR 2005. LNCS, vol.\u00a03524, pp. 288\u2013303. Springer, Heidelberg (2005)"},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C. Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 827\u2013831. Springer, Heidelberg (2005)"},{"key":"14_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"O. Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol.\u00a02833, pp. 108\u2013122. Springer, Heidelberg (2003)"},{"key":"14_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-02777-2_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"R. As\u00edn","year":"2009","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks and their applications. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 167\u2013180. Springer, Heidelberg (2009)"},{"key":"14_CR32","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":"14_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"618","DOI":"10.1007\/978-3-540-71209-1_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Condrat","year":"2007","unstructured":"Condrat, C., Kalla, P.: A gr\u00f6bner basis approach to CNF-formulae preprocessing. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 618\u2013631. Springer, Heidelberg (2007)"},{"issue":"3-5","key":"14_CR34","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/S0167-6377(98)00052-2","volume":"23","author":"J.P. Warners","year":"1998","unstructured":"Warners, J.P., van Maaren, H.: A two-phase algorithm for solving a class of hard satisfiability problems. Operations Research Letters\u00a023(3-5), 81\u201388 (1998)","journal-title":"Operations Research Letters"},{"issue":"3","key":"14_CR35","doi-asserted-by":"publisher","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. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"14_CR36","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":"1\/2","key":"14_CR37","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1023\/A:1006370506164","volume":"24","author":"W. K\u00fcchlin","year":"2000","unstructured":"K\u00fcchlin, W., Sinz, C.: Proving consistency assertions for automotive product data management. J. Autom. Reasoning\u00a024(1\/2), 145\u2013163 (2000)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"14_CR38","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1023\/A:1009812409930","volume":"4","author":"B. Cabon","year":"1999","unstructured":"Cabon, B., de Givry, S., Lobjois, L., Schiex, T., Warners, J.P.: Radio link frequency assignment. Constraints\u00a04(1), 79\u201389 (1999)","journal-title":"Constraints"},{"key":"14_CR39","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/SAT190075","volume":"7","author":"D. Berre Le","year":"2010","unstructured":"Le Berre, D., Parrain, A.: The sat4j library, release 2.2, system description. Journal on Satisfiability, Boolean Modeling and Computation (JSAT)\u00a07, 59\u201364 (2010)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation (JSAT)"},{"key":"14_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-642-04238-6_50","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M. Gebser","year":"2009","unstructured":"Gebser, M., Kaufmann, B., Schaub, T.: The conflict-driven answer set solver clasp: Progress report. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol.\u00a05753, pp. 509\u2013514. Springer, Heidelberg (2009)"},{"key":"14_CR41","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":"14_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-31612-8_47","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M.H. Liffiton","year":"2012","unstructured":"Liffiton, M.H., Maglalang, J.C.: A cardinality solver: More expressive constraints for free - (poster presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 485\u2013486. Springer, Heidelberg (2012)"},{"issue":"1","key":"14_CR43","first-page":"565","volume":"32","author":"L. Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla: portfolio-based algorithm selection for sat. J. Artif. Int. Res.\u00a032(1), 565\u2013606 (2008)","journal-title":"J. Artif. Int. Res."},{"key":"14_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-72788-0_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"S.D. Prestwich","year":"2007","unstructured":"Prestwich, S.D.: Variable Dependency in Local Search: Prevention Is Better Than Cure. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 107\u2013120. Springer, Heidelberg (2007)"},{"key":"14_CR45","unstructured":"Chen, J.: A New SAT Encoding of the At-Most-One Constraint. In: Proceedings of ModRef 2011 (2011)"},{"key":"14_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-31612-8_30","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"Y. Ben-Haim","year":"2012","unstructured":"Ben-Haim, Y., Ivrii, A., Margalit, O., Matsliah, A.: Perfect hashing and CNF encodings of cardinality constraints. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 397\u2013409. Springer, Heidelberg (2012)"},{"key":"14_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-02777-2_3","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M.L. Bonet","year":"2009","unstructured":"Bonet, M.L., John, K.S.: Efficiently calculating evolutionary tree measures using SAT. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 4\u201317. Springer, Heidelberg (2009)"},{"key":"14_CR48","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-21043-3_5","volume-title":"Advances in Artificial Intelligence","author":"C. Anton","year":"2011","unstructured":"Anton, C.: An improved satisfiable SAT generator based on random subgraph isomorphism. In: Butz, C., Lingras, P. (eds.) Canadian AI 2011. LNCS (LNAI), vol.\u00a06657, pp. 44\u201349. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39611-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,2]],"date-time":"2023-07-02T17:44:31Z","timestamp":1688319871000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39611-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396106","9783642396113"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39611-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}