{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:42:31Z","timestamp":1762101751696,"version":"3.41.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243177"},{"type":"electronic","value":"9783319243184"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24318-4_19","type":"book-chapter","created":{"date-parts":[[2015,9,11]],"date-time":"2015-09-11T05:42:56Z","timestamp":1441950176000},"page":"255-271","source":"Crossref","is-referenced-by-count":3,"title":["Recognition of Nested Gates in CNF Formulas"],"prefix":"10.1007","author":[{"given":"Markus","family":"Iser","sequence":"first","affiliation":[]},{"given":"Norbert","family":"Manthey","sequence":"additional","affiliation":[]},{"given":"Carsten","family":"Sinz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,27]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Balint, A., Manthey, N.: Boosting the performance of SLS and CDCL solvers by preprocessor tuning. In: Berre, D.L. (ed.) POS 2013. EPiC Series, vol. 29, pp. 1\u201314. EasyChair (2014)","DOI":"10.29007\/28ww"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/978-3-319-09284-3_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"T Balyo","year":"2014","unstructured":"Balyo, T., Fr\u00f6hlich, A., Heule, M.J.H., Biere, A.: Everything you always wanted to know about blocked sets (but were afraid to ask). In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 317\u2013332. Springer, Heidelberg (2014)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/978-3-319-09284-3_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"A Biere","year":"2014","unstructured":"Biere, A., Le Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 285\u2013301. Springer, Heidelberg (2014). http:\/\/dx.doi.org\/10.1007\/978-3-319-09284-3_22"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-540-24605-3_24","volume-title":"Theory and Applications of Satisfiability Testing","author":"P Bjesse","year":"2004","unstructured":"Bjesse, P., Kukula, J.H., Damiano, R., Stanion, T., Zhu, Y.: Guiding SAT diagnosis with tree decompositions. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 315\u2013329. Springer, Heidelberg (2004)"},{"issue":"5","key":"19_CR5","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"issue":"3","key":"19_CR6","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 7(3), 201\u2013215 (1960). http:\/\/doi.acm.org\/10.1145\/321033.321034","journal-title":"Journal of the ACM"},{"key":"19_CR7","unstructured":"Dixon, H.E., Ginsberg, M.L., Luks, E.M., Parkes, A.J.: Generalizing Boolean satisfiability II: Theory (2011). CoRR abs\/1109.2134"},{"key":"19_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. 3569, pp. 61\u201375. Springer, Heidelberg (2005). http:\/\/dx.doi.org\/10.1007\/11499107_5"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1007\/978-3-642-36742-7_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Falke","year":"2013","unstructured":"Falke, S., Merz, F., Sinz, C.: LLBMC: improved bounded model checking of C programs using LLVM (competition contribution). In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 623\u2013626. Springer, Heidelberg (2013)"},{"key":"19_CR10","unstructured":"Fu, Z., Malik, S.: Extracting logic circuit structure from conjunctive normal form descriptions. In: 20th International Conference on VLSI Design (VLSI Design 2007), Sixth International Conference on Embedded Systems (ICES 2007), January 6\u201310, 2007, Bangalore, India. pp. 37\u201342 (2007)"},{"key":"19_CR11","unstructured":"Fu, Z., Yu, Y., Malik, S.: Considering circuit observability don\u2019t cares in CNF satisfiability. In: 2005 Design, Automation and Test in Europe Conference and Exposition (DATE 2005), March 7\u201311, 2005, Munich, Germany, pp. 1108\u20131113 (2005)"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-642-45221-5_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"MJH Heule","year":"2013","unstructured":"Heule, M.J.H., Biere, A.: Blocked clause decomposition. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 423\u2013438. Springer, Heidelberg (2013). http:\/\/dx.doi.org\/10.1007\/978-3-642-45221-5_29"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-39071-5_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"M Iser","year":"2013","unstructured":"Iser, M., Sinz, C., Taghdiri, M.: Minimizing models for tseitin-encoded SAT instances. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 224\u2013232. Springer, Heidelberg (2013)"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-642-31612-8_46","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M Iser","year":"2012","unstructured":"Iser, M., Taghdiri, M., Sinz, C.: Optimizing MiniSAT variable orderings for the relational model finder kodkod (poster presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 483\u2013484. Springer, Heidelberg (2012)"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129\u2013144. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Simulating circuit-level simplifications on cnf. Journal of Automated Reasoning 49(4), 583\u2013619 (2012)","DOI":"10.1007\/s10817-011-9239-9"},{"issue":"12","key":"19_CR17","doi-asserted-by":"publisher","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. on CAD of Integrated Circuits and Systems 21(12), 1377\u20131394 (2002)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-31612-8_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"N Manthey","year":"2012","unstructured":"Manthey, N.: Coprocessor 2.0 \u2013 a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 436\u2013441. Springer, Heidelberg (2012). http:\/\/dx.doi.org\/10.1007\/978-3-642-31612-8_34"},{"key":"19_CR19","unstructured":"Manthey, N.: Extended resolution in modern SAT solving. In: Joint Automated Reasoning Workshop and Deduktionstreffen (2014)"},{"key":"19_CR20","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. 7857, pp. 102\u2013117. Springer, Heidelberg (2013). http:\/\/dx.doi.org\/10.1007\/978-3-642-39611-3_14"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-39071-5_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"A Mihal","year":"2013","unstructured":"Mihal, A., Teig, S.: A constraint satisfaction approach for programmable logic detailed placement. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 208\u2013223. Springer, Heidelberg (2013)"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/3-540-46135-3_13","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"RO\u00c9 Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, R.O.\u00c9., Sa\u00efs, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, p. 185. Springer, Heidelberg (2002)"},{"issue":"3","key":"19_CR23","doi-asserted-by":"publisher","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."},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Rintanen, J.: Engineering efficient planners with SAT. In: ECAI, pp. 684\u2013689 (2012)","DOI":"10.3233\/978-1-61499-098-7-684"},{"issue":"2","key":"19_CR25","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-007-9074-1","volume":"39","author":"C Sinz","year":"2007","unstructured":"Sinz, C.: Visualizing SAT instances and runs of the DPLL algorithm. J. Autom. Reasoning 39(2), 219\u2013243 (2007)","journal-title":"J. Autom. Reasoning"},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"19_CR27","unstructured":"Boy de la Tour, T.: An optimality result for clause form translation. J. Symb. Comput. 14(4), 283\u2013301 (1992)"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, pp. 115\u2013125 (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"19_CR29","unstructured":"Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: IJCAI, pp. 1173\u20131178 (2003)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing -- SAT 2015"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24318-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T15:26:35Z","timestamp":1748618795000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24318-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243177","9783319243184"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24318-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}