Name
Abstract | ||
|---|---|---|
Quantified Boolean satisfiability (QSAT) is natural formulation of many decision problems and yet awaits further breakthroughs to reach the maturity enabling industrial applications. Recent advancements on quantified Boolean formula (QBF) proof systems sharpen our understanding of their proof complexities and shed light on solver improvement. Particularly QBF solving based on formula expansion has been theoretically and practically demonstrated to be more powerful than non-expansion based solving. However recursive expansion suffers from exponential formula explosion and has to be carefully managed. In this paper, we propose a QBF solver using levelized SAT solving in the flavor of formula expansion. New learning techniques based on circuit structure reconstruction, complete and incomplete ALLSAT learning, core expansion, bounded recursion, and other methods are devised to control formula growth. Experimental results on application benchmarks show that our prototype implementation is comparable with state-of-the-art solvers and outperforms other solvers in certain instances. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-24318-4_25 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Discrete mathematics,Decision problem,Computer science,Boolean satisfiability problem,Algorithm,Theoretical computer science,Solver,True quantified Boolean formula,Recursion,Bounded function,Exponential formula | Conference | 9340 |
ISSN | Citations | PageRank |
0302-9743 | 8 | 0.49 |
References | Authors | |
14 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kuan-Hua Tu | 1 | 11 | 1.22 |
| Tzu-Chien Hsu | 2 | 8 | 0.49 |
| Jie-Hong R. Jiang | 3 | 353 | 37.47 |