Proving that there are problems in $P^{NP}$ that require boolean circuits of super-linear size is a major frontier in complexity theory. While such lower bounds are known for larger complexity classes, existing results only show that the corresponding problems are hard on infinitely many input lengths. For instance, proving almost-everywhere ... more >>>

The solving of Quantified Boolean Formulas (QBF) has been advanced considerably in the last two decades. In response to this, several proof systems have been put forward to universally verify QBF solvers.
QRAT by Heule et al. is one such example of this and builds on technology from DRAT, ... more >>>

Relations and Equivalences Between Circuit Lower Bounds and Karp-Lipton Theorems

A frontier open problem in circuit complexity is to prove P^NP is not in SIZE[n^k] for all k; this is a necessary intermediate step towards NP is not in P/poly. Previously, for several classes containing P^NP, including NP^NP, ZPP^NP, and ... more >>>