Name
Abstract | ||
|---|---|---|
Resolution proof systems for quantified Boolean formulas (QBFs) provide a formal model for studying the limitations of state-of-the-art search-based QBF solvers, which use these systems to generate proofs. In this paper, we define a new proof system that combines two such proof systems: Q-resolution with generalized universal reduction according to a dependency scheme and long distance Q-resolution. We show that the resulting proof system is sound for the reflexive resolution-path dependency scheme-in fact, we prove that it admits strategy extraction in polynomial time. As a special case, we obtain soundness and polynomial-time strategy extraction for long distance Q-resolution with universal reduction according to the standard dependency scheme. We report on experiments with a configuration of DepQBF that generates proofs in this system. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-40970-2_31 | Lecture Notes in Computer Science |
DocType | Volume | ISSN |
Conference | 9710 | 0302-9743 |
Citations | PageRank | References |
3 | 0.37 | 31 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tomás Peitl | 1 | 6 | 4.82 |
| Friedrich Slivovsky | 2 | 62 | 7.96 |
| Stefan Szeider | 3 | 1341 | 99.97 |