Name
Abstract | ||
|---|---|---|
We describe a novel decision procedure for Quantified Boolean Formulas (QBFs) which aims to unleash the hidden potential of quantified reasoning in applications. The Skolem theorem acts like a glue holding several ingredients together: BDD-based representations for boolean functions, search-based QBF decision procedure, and compilation-to-SAT techniques, among the others. To leverage all these techniques at once we show how to evaluate QBFs by symbolically reasoning on a compact representation for the propositional expansion of the skolemized problem. We also report about a first implementation of the procedure, which yields very interesting experimental results. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/978-3-540-32275-7_20 | Lecture Notes in Artificial Intelligence |
Keywords | Field | DocType |
boolean function | Boolean function,Computer science,Algorithm,Theoretical computer science,Conjunctive normal form,True quantified Boolean formula,Skolem normal form | Conference |
Volume | ISSN | Citations |
3452 | 0302-9743 | 31 |
PageRank | References | Authors |
1.58 | 27 | 1 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marco Benedetti | 1 | 31 | 2.60 |