ECCC-Report TR19-157https://eccc.weizmann.ac.il/report/2019/157Comments and Revisions published for TR19-157en-usSun, 10 Nov 2019 08:56:13 +0200
Paper TR19-157
| How QBF Expansion Makes Strategy Extraction Hard |
Judith Clymo,
Leroy Chew
https://eccc.weizmann.ac.il/report/2019/157In this paper we show that the QBF proof checking format QRAT (Quantified Resolution Asymmetric Tautologies) by Heule, Biere and Seidl cannot have polynomial-time strategy extraction unless P=PSPACE. In our proof, the crucial property that makes strategy extraction PSPACE-hard for this proof format is universal expansion, even expansion on a single variable.
While expansion reasoning used in other QBF calculi can admit polynomial time strategy extraction, we find this is conditional on a property studied in proof complexity theory. We show that strategy extraction on expansion based systems can only happen when the underlying propositional calculus has the property of feasible interpolation. Sun, 10 Nov 2019 08:56:13 +0200https://eccc.weizmann.ac.il/report/2019/157