Yijia Chen, Joerg Flum

We prove that TAUT has a $p$-optimal proof system if and only if $L_\le$, a logic introduced in [Gurevich, 88], is a P-bounded logic for P. Furthermore, using the method developed in [Chen and Flum, 10], we show that TAUT has no \emph{effective} $p$-optimal proof system under some reasonable complexity-theoretic ... more >>>

Paul Goldberg, Christos Papadimitriou

The complexity class TFNP is the set of {\em total function} problems that belong to NP: every input has at least one output and outputs are easy to check for validity, but it may be hard to find an output. TFNP is not believed to have complete problems, but it ... more >>>

Sam Buss, Dmitry Itsykson, Alexander Knop, Artur Riazanov, Dmitry Sokolov

This paper is motivated by seeking lower bounds on OBDD($\land$, weakening, reordering) refutations, namely OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1-NBP($\land$) refutations based on read-once nondeterministic branching programs. These generalize OBDD($\land$, reordering) refutations. There are polynomial size 1-NBP($\land$) refutations of the pigeonhole principle, hence ... more >>>

Sravanthi Chede, Leroy Chew, Balesh Kumar, Anil Shukla

QBF proof systems are routinely adapted from propositional logic along with adjustments for the new quantifications. Existing are two main successful frameworks, the reduction and expansion frameworks, inspired by QCDCL [Zhang et al. ICCAD.'2002] and CEGAR solving [Janota et al. Artif. Intell.'2016] respectively. However, the reduction framework, while immensely useful ... more >>>