Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with Strategy extraction:
TR14-120 | 16th September 2014
Olaf Beyersdorff, Leroy Chew, Mikolas Janota

Proof Complexity of Resolution-based QBF Calculi

Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of important
QBF solvers. However, the proof complexity of these proof systems is currently not well understood and in particular
lower bound techniques are missing. In this paper we exhibit a new and elegant proof technique ... more >>>

TR16-011 | 27th January 2016
Olaf Beyersdorff, Ján Pich

Understanding Gentzen and Frege systems for QBF

Recently Beyersdorff, Bonacina, and Chew (ITCS'16) introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. Here we provide a comprehensive analysis of the new extended Frege system from Beyersdorff et al., denoted EF+$\forall$red, which is 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 >>>

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

TR20-159 | 9th October 2020
Leroy Chew, Marijn Heule

Relating existing powerful proof systems for QBF

We advance the theory of QBF proof systems by showing the first simulation of the universal checking format QRAT by a theory-friendly system. We show that the sequent system G fully p-simulates QRAT, including the Extended Universal Reduction (EUR) rule which was recently used to show QRAT does not ... more >>>

ISSN 1433-8092 | Imprint