Name
Abstract | ||
|---|---|---|
Davis-Putnam resolution is one of the fundamental theoretical decision procedures for both propositional logic and quantified Boolean formulas. Dependency quantified Boolean formulas (DQBF) are a generalisation of QBF in which dependencies of variables are listed explicitly rather than being implicit in the order of quantifiers. Since DQBFs can succinctly encode synthesis problems that ask for Boolean functions matching a given specification, efficient DQBF solvers have a wide range of potential applications. We present a new decision procedure for DQBF in the style of Davis-Putnam resolution. Based on the merge resolution proof system, it directly constructs partial strategy functions for derived clauses. The procedure requires DQBF in a normal form called H-Form. We prove that the problem of evaluating DQBF in H-Form is NEXP-complete. In fact, we show that any DQBF can be converted into H-Form in linear time. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1007/978-3-030-80223-3_4 | THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, SAT 2021 |
DocType | Volume | ISSN |
Conference | 12831 | 0302-9743 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Joshua Blinkhorn | 1 | 3 | 6.16 |
| Tomás Peitl | 2 | 6 | 4.82 |
| Friedrich Slivovsky | 3 | 0 | 1.01 |