Name
Abstract | ||
|---|---|---|
We consider the problem of QBF solving viewed as a reachability problem in an exponential And-Or graph. Antichain-based algorithms for reachability analysis in large graphs exploit certain subsumption relations to leverage the inherent structure of the explored graph in order to reduce the effect of state explosion, with high performance in practice. In this paper, we propose simple notions of subsumption induced by the structural properties of the And-Or graphs for QBF solving. Subsumption is used to reduce the size of the search tree, and to define compact representations of certificates (in the form of antichains) both for positive and negative instances of QBF. We show that efficient exploration of the reduced search tree essentially relies on solving variants of Max-SAT and Min-SAT. Preliminary stand-alone experiments of this algorithm show that the antichain-based approach is promising. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-24372-1_14 | ATVA |
Keywords | Field | DocType |
reduced search tree,reachability analysis,search tree,antichain-based qbf,certain subsumption relation,exponential and-or graph,algorithm show,explored graph,and-or graph,reachability problem,large graph | Discrete mathematics,Antichain,Exponential function,Computer science,Binary decision diagram,Algorithm,Reachability,Theoretical computer science,Exploit,Reachability problem,True quantified Boolean formula,Search tree | Conference |
Volume | ISSN | Citations |
6996 | 0302-9743 | 1 |
PageRank | References | Authors |
0.35 | 22 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thomas Brihaye | 1 | 460 | 35.91 |
| Véronique Bruyère | 2 | 429 | 43.59 |
| Lauren Doyen | 3 | 1 | 0.35 |
| Marc Ducobu | 4 | 4 | 1.12 |
| Jean-Francois Raskin | 5 | 115 | 7.17 |