2026-07-23T16:50:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27050 2026-07-23T11:36:18Z ddc:004 open_access

Efficient Adversaries Khaniki, Erfan Pich, Ján Sokolov, Dmitry proof complexity circuit complexity lower bounds barriers truth-table formula pigeonhole principle The size of Frege proofs can be characterized in terms of prover-adversary games of Pudlák and Buss. We consider a generalization of prover-adversary games to many standard proof systems and show that some of the major proof complexity lower bounds such as the constant-depth Frege lower bound for the pigeonhole principle based on the method of k-evaluations, the Resolution lower bound for the weak pigeonhole principle based on the method of pseudo-width and Razborov’s Res(k) lower bound for Nisan-Wigderson generators based on expansion and a width lower bound (which is used to derive the Res(k)-hardness of formulas expressing circuit lower bounds) are constructive in the sense that they yield efficient algorithms computing winning strategies of adversaries in the generalized games. This is in contrast with our second result saying that if (a) such a constructive lower bound exists for Extended Frege system EF for formulas expressing succinct circuit lower bounds for SAT and (b) EF is strong enough to prove efficiently the correctness of anticheckers for SAT, then it is easy to separate the canonical pair of EF. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Erfan Khaniki and Ján Pich and Dmitry Sokolov 2026 Is Part Of LIPIcs, Volume 383, 41st Computational Complexity Conference (CCC 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CCC.2026.8 urn:nbn:de:0030-drops-270508 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2026.8 eng https://creativecommons.org/licenses/by/4.0/legalcode