{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:02:00Z","timestamp":1777125720166,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540797180","type":"print"},{"value":"9783540797197","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79719-7_19","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T04:04:57Z","timestamp":1210046697000},"page":"196-210","source":"Crossref","is-referenced-by-count":23,"title":["Nenofex: Expanding NNF for QBF Solving"],"prefix":"10.1007","author":[{"given":"Florian","family":"Lonsing","sequence":"first","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","volume-title":"Essentials of Electronic Testing for Digital, Memory and Mixed-Signal VLSI Circuits","author":"V. Agrawal","year":"2000","unstructured":"Agrawal, V., Bushnell, M.: Essentials of Electronic Testing for Digital, Memory and Mixed-Signal VLSI Circuits. Kluwer, Dordrecht (2000)"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Ayari","year":"2002","unstructured":"Ayari, A., Basin, D.A.: QUBOS: Deciding quantified boolean logic using propositional satisfiability solvers. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, Springer, Heidelberg (2002)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/11499107_28","volume-title":"Theory and Applications of Satisfiability Testing","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: Quantifier Trees for QBFs. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 378\u2013385. Springer, Heidelberg (2005)"},{"key":"19_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/11532231_27","volume-title":"Automated Deduction \u2013 CADE-20","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: sKizzo: A Suite to Evaluate and Certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"key":"19_CR5","unstructured":"Benedetti, M.: Experimenting with QBF-based formal verification. In: Proc.\u00a0CFV 2005 (2005)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, Springer, Heidelberg (1999)"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Bor\u00e4lv, A.: DAG-aware circuit compression for formal verification. In: Proc.\u00a0ICCAD 2004 (2004)","DOI":"10.1109\/ICCAD.2004.1382541"},{"key":"19_CR9","unstructured":"Brummayer, R., Biere, A.: Local two-level and-inverter graph minimization without blowup. In: Proc.\u00a0MEMICS 2006 (2006)"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-540-72788-0_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"U. Bubeck","year":"2007","unstructured":"Bubeck, U., Kleine B\u00fcning, H.: Bounded Universal Expansion for Preprocessing QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 244\u2013257. Springer, Heidelberg (2007)"},{"key":"19_CR11","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified boolean formulae. In: Proc.\u00a0AAAI\/IAAI 1998 (1998)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Darwiche, A.: Decomposable negation normal form. JACM\u00a048(4) (2001)","DOI":"10.1145\/502090.502091"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. CACM\u00a05(7) (1962)","DOI":"10.1145\/368273.368557"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. JACM\u00a07(3) (1960)","DOI":"10.1145\/321033.321034"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Boy de la Tour, T.: An optimality result for clause form translation. Symb.\u00a0Comput.\u00a014(4) (1992)","DOI":"10.1016\/0747-7171(92)90009-S"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11499107_4","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Dershowitz","year":"2005","unstructured":"Dershowitz, N., Hanna, Z., Katz, J.: Bounded Model Checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 408\u2013414. Springer, Heidelberg (2005)"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1007\/978-3-540-24605-3_17","volume-title":"Theory and Applications of Satisfiability Testing","author":"U. Egly","year":"2004","unstructured":"Egly, U., Seidl, M., Tompits, H., Woltran, S., Zolda, M.: Comparing Different Prenexing Strategies for Quantified Boolean Formulas. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 214\u2013228. Springer, Heidelberg (2004)"},{"key":"19_CR19","unstructured":"Garey, M., Johnson, D.: Computers and Intractability: A Guide to the Theory of NP-Completeness (1979)"},{"key":"19_CR20","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for quantified boolean logic satisfiability. In: Proc.\u00a0AAAI 2002 (2002)"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/11527695_9","volume-title":"Theory and Applications of Satisfiability Testing","author":"E. Giunchiglia","year":"2005","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QBF Reasoning on Real-World Instances. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 105\u2013121. Springer, Heidelberg (2005)"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantifier structure in search based procedures for QBFs. In: Proc.\u00a0DATE 2006 (2006)","DOI":"10.1109\/DATE.2006.244148"},{"key":"19_CR23","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantified Boolean Formulas satisfiability library (QBFLIB) (2001), www.qbflib.org"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Jussila, T., Biere, A.: Compressing BMC encodings with QBF. In: Proc.\u00a0BMC 2006 (2006)","DOI":"10.1016\/j.entcs.2006.12.022"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Kleine B\u00fcning, H., Karpinski, M., Fl\u00fcgel, A.: Resolution for quantified boolean formulas. Inf.\u00a0Comput.\u00a0117(1) (1995)","DOI":"10.1006\/inco.1995.1025"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. TCAD\u00a021(12) (2002)","DOI":"10.1109\/TCAD.2002.804386"},{"key":"19_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2572-8","volume-title":"Reasoning in Boolean Networks: Logic Synthesis and Verification Using Testing Techniques","author":"W. Kunz","year":"1997","unstructured":"Kunz, W., Stoffel, D.: Reasoning in Boolean Networks: Logic Synthesis and Verification Using Testing Techniques. Kluwer, Dordrecht (1997)"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Ladner, R.: The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing\u00a06(3) (1977)","DOI":"10.1137\/0206033"},{"key":"19_CR29","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R.: Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, Springer, Heidelberg (2002)"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Mangassarian, H., Veneris, A., Safarpour, S., Benedetti, M., Smith, D.: A performance-driven QBF-based iterative logic array representation with applications to verification, debug and test. In: Proc.\u00a0ICCAD 2007 (2007)","DOI":"10.1109\/ICCAD.2007.4397272"},{"key":"19_CR31","unstructured":"Otwell, C., Remshagen, A., Truemper, K.: An effective QBF solver for planning problems. In: MSV\/AMCS (2004)"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. Symb.\u00a0Comput.\u00a02(3) (1986)","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"Rintanen, J.: Constructing conditional plans by a theorem-prover. Journal of Artificial Intelligence Research\u00a010 (1999)","DOI":"10.1613\/jair.591"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Sabharwal, A., Ans\u00f3tegui, C., Gomes, C., Hart, J., Selman, B.: QBF modeling: Exploiting player symmetry for simplicity and efficiency. In: Proc.\u00a0SAT 2006 (2006)","DOI":"10.1007\/11814948_35"},{"key":"19_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-540-72788-0_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"M. Samer","year":"2007","unstructured":"Samer, M., Szeider, S.: Backdoor Sets of Quantified Boolean Formulas. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 230\u2013243. Springer, Heidelberg (2007)"},{"key":"19_CR36","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.: The polynomial\u2013time hierarchy. TCS\u00a03(1) (1976)","DOI":"10.1016\/0304-3975(76)90061-X"},{"key":"19_CR37","series-title":"Lecture Notes in Computer Science","first-page":"368","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"S. Malik","year":"2006","unstructured":"Malik, S., Tang, D.: Solving Quantified Boolean Formulas with Circuit Observability Don\u2019t Cares. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 368\u2013381. Springer, Heidelberg (2006)"},{"key":"19_CR38","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic\u00a02 (1968)"},{"key":"19_CR39","unstructured":"Zhang, L.: Solving QBF by combining conjunctive and disjunctive normal forms. In: Proc.\u00a0AAAI 2006 (2006)"},{"key":"19_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-46027-6","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79719-7_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,18]],"date-time":"2023-05-18T00:28:01Z","timestamp":1684369681000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79719-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797180","9783540797197"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79719-7_19","relation":{},"subject":[]}}