Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR19-157 | 25th September 2019 16:56

How QBF Expansion Makes Strategy Extraction Hard

RSS-Feed




TR19-157
Authors: Leroy Chew, Judith Clymo
Publication: 10th November 2019 08:56
Downloads: 1071
Keywords: 


Abstract:

In 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.



ISSN 1433-8092 | Imprint