Name
Abstract | ||
|---|---|---|
The majority of the currently available solvers for quantified Boolean formulas (QBFs) process input formulas only in prenex conjunctive normal form. However, the natural representation of practicably relevant problems in terms of QBFs usually results in formulas which are not in a specific normal form. Hence, in order to evaluate such QBFs with available solvers, suitable normal-form translations are required. In this paper, we report experimental results comparing different prenexing strategies on a class of structured benchmark problems. The problems under consideration encode the evaluation of nested counterfactuals over a propositional knowledge base, and span the entire polynomial hierarchy. The results show that different prenexing strategies influence the evaluation time in different ways across different solvers. In particular, some solvers are robust to the chosen strategies while others are not. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1007/978-3-540-24605-3_17 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
knowledge base,conjunctive normal form,normal form | Polynomial hierarchy,ENCODE,Constraint satisfaction,Discrete mathematics,Descriptive knowledge,Combinatorics,Computer science,Satisfiability,Conjunctive normal form,Counterfactual conditional,Knowledge base | Conference |
Volume | ISSN | Citations |
2919 | 0302-9743 | 24 |
PageRank | References | Authors |
0.84 | 17 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Uwe Egly | 1 | 544 | 45.57 |
| Martina Seidl | 2 | 685 | 51.78 |
| Hans Tompits | 3 | 1916 | 97.73 |
| Stefan Woltran | 4 | 1603 | 121.99 |
| Michael Zolda | 5 | 42 | 3.57 |