[Zurück]

L. Chew:
"Hardness and Optimality for QBF Proof Systems Modulo NP";
Vortrag: International Conference on the Theory and Applications of Satisfiability Testing, Barcelona; 05.07.2021 - 09.07.2021; in: "SAT 2021: Theory and Applications of Satisfiability Testing - SAT 2021", Springer, 12831 (2021), ISBN: 978-3-030-80223-3; S. 98 - 115.

In this paper we show that extended Q-resolution is optimal
among all QBF proof systems that allow strategy extraction modulo an
NP oracle. In other words, for any QBF refutation system f where circuits
witnessing the Herbrand functions can be extracted in polynomial
time from f-refutations, f can be simulated by extended Q-resolution
augmented with an NP oracle as described by Beyersdor et al.We argue
that using NP oracles and strategy extraction gives a natural framework
to study QBF systems as they have relations to SAT calls and game
instances, respectively, in QBF solving.
A weaker version of QBF extension variables also put forward by Jussila
et al. does not have this optimality result, and we show that under an NP
oracle there is no improvement of weak extended Q-Resolution compared
to ordinary Q-Resolution.

http://dx.doi.org/10.1007/978-3-030-80223-3_8

https://publik.tuwien.ac.at/files/publik_299254.pdf