All reports by Author Leroy Chew:

__
TR23-053
| 19th April 2023
__

Leroy Chew#### Proof Simulation via Round-based Strategy Extraction for QBF

__
TR21-144
| 13th October 2021
__

Leroy Chew, Friedrich Slivovsky#### Towards Uniform Certification in QBF

__
TR20-159
| 9th October 2020
__

Leroy Chew, Marijn Heule#### Relating existing powerful proof systems for QBF

__
TR19-157
| 25th September 2019
__

Leroy Chew, Judith Clymo#### How QBF Expansion Makes Strategy Extraction Hard

__
TR18-178
| 9th October 2018
__

Leroy Chew#### Hardness and Optimality in QBF Proof Systems Modulo NP

Leroy Chew

The proof complexity of Quantified Boolean Formulas (QBF) relates to both QBF solving and OBF certification. One method to p-simulate a QBF proof system is by formalising the soundness of its strategy extraction in propositional logic. In this work we illustrate how to use extended QBF Frege to simulate LD-Q(Drrs)-Res, ... more >>>

Leroy Chew, Friedrich Slivovsky

We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q-Resolution, and Merge Resolution.

These results are obtained by taking a technique ...
more >>>

Leroy Chew, Marijn Heule

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

Leroy Chew, Judith Clymo

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

Leroy Chew

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