Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > AUTHORS > LEROY CHEW:
All reports by Author Leroy Chew:

TR19-157 | 25th September 2019
Leroy Chew, Judith Clymo

How QBF Expansion Makes Strategy Extraction Hard

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


TR18-178 | 9th October 2018
Leroy Chew

Hardness and Optimality in QBF Proof Systems Modulo NP

Quantified Boolean Formulas (QBFs) extend propositional formulas with Boolean quantifiers. Working with QBF differs from propositional logic in its quantifier handling, but as propositional satisfiability (SAT) is a subproblem of QBF, all SAT hardness in solving and proof complexity transfers to QBF. This makes it difficult to analyse efforts dealing ... more >>>




ISSN 1433-8092 | Imprint