Solving QBF with Free Variables
作者： William Klieber , Mikoláš Janota , Joao Marques-Silva , Edmund Clarke
DOI: 10.1007/978-3-642-40627-0_33
关键词: Of the form 、 Discrete mathematics 、 Logical equivalence 、 Class (set theory) 、 True quantified Boolean formula 、 DPLL algorithm 、 Mathematics 、 Free variables and bound variables 、 Rule of inference 、 Cube
摘要: An open quantified boolean formula QBF is a that contains free unquantified variables. A solution to such quantifier-free logically equivalent the given QBF. Although most recent research has focused on closed QBF, there are number of interesting applications require one consider formulas with This article shows how clause/cube learning for DPLL-based closed-QBF solvers can be extended solve QBFs We do this by introducing sequents generalize clauses and cubes allow facts form "under certain class assignments, input formula".
springer.com
sci-hub.st 参考文章(30)
Bart Selman, Carla P. Gomes, Carlos Ansotegui, The achilles' heel of QBF national conference on artificial intelligence. pp. 275- 281 ,(2005)
Alexandra Goultiaeva, Fahiem Bacchus, Exploiting QBF duality on a circuit representation national conference on artificial intelligence. pp. 71- 76 ,(2010)
Lintao Zhang, Solving QBF with combined conjunctive and disjunctive normal form national conference on artificial intelligence. pp. 143- 149 ,(2006)
Bernd Becker, Rüdiger Ehlers, Matthew Lewis, Paolo Marin, ALLQBF Solving by Computational Learning Automated Technology for Verification and Analysis. pp. 370- 384 ,(2012) , 10.1007/978-3-642-33386-6_29
Lintao Zhang, Solving QBF by Combining Conjunctive and Disjunctive Normal Forms. national conference on artificial intelligence. pp. 143- 150 ,(2006)
Jörg Brauer, Andy King, Jael Kriener, Existential quantification as incremental SAT computer aided verification. pp. 191- 207 ,(2011) , 10.1007/978-3-642-22110-1_17
Universitet u Nišu, Facta universitatis. Series, electronics and energetics University of Niš. ,(1988)
Marco Benedetti, sKizzo: a suite to evaluate and certify QBFs conference on automated deduction. pp. 369- 376 ,(2005) , 10.1007/11532231_27
Ian Gent, Enrico Giunchiglia, Massimo Narizzano, Andrew Rowley, Armando Tacchella, Watched Data Structures for QBF Solvers theory and applications of satisfiability testing. pp. 25- 36 ,(2003) , 10.1007/978-3-540-24605-3_3
Marco Benedetti, Hratch Mangassarian, QBF-Based Formal Verification: Experience and Perspectives Journal on Satisfiability, Boolean Modeling and Computation. ,vol. 5, pp. 133- 191 ,(2008) , 10.3233/SAT190055