Derandomizing Arthur-Merlin Games and Approximate Counting Implies Exponential-Size Lower Bounds

Computational Complexity ◽

10.1007/s00037-011-0010-8 ◽

2011 ◽

Vol 20 (2) ◽

pp. 329-366 ◽

Cited By ~ 6

Author(s):

Barış Aydınlıog̃lu ◽

Dan Gutfreund ◽

John M. Hitchcock ◽

Akinori Kawachi

Keyword(s):

Lower Bounds ◽

Approximate Counting ◽

Exponential Size

Download Full-text

Computational and Proof Complexity of Partial String Avoidability

ACM Transactions on Computation Theory ◽

10.1145/3442365 ◽

2021 ◽

Vol 13 (1) ◽

pp. 1-25

Author(s):

Dmitry Itsykson ◽

Alexander Okhotin ◽

Vsevolod Oparin

Keyword(s):

Lower Bounds ◽

Circuit Complexity ◽

Conjunctive Normal Form ◽

Proof Complexity ◽

Proof Systems ◽

Finite Set ◽

Propositional Proof Systems ◽

Classical Proof ◽

Exponential Size ◽

Infinite String

The partial string avoidability problem is stated as follows: given a finite set of strings with possible “holes” (wildcard symbols), determine whether there exists a two-sided infinite string containing no substrings from this set, assuming that a hole matches every symbol. The problem is known to be NP-hard and in PSPACE, and this article establishes its PSPACE-completeness. Next, string avoidability over the binary alphabet is interpreted as a version of conjunctive normal form satisfiability problem, where each clause has infinitely many shifted variants. Non-satisfiability of these formulas can be proved using variants of classical propositional proof systems, augmented with derivation rules for shifting proof lines (such as clauses, inequalities, polynomials, etc.). First, it is proved that there is a particular formula that has a short refutation in Resolution with a shift rule but requires classical proofs of exponential size. At the same time, it is shown that exponential lower bounds for classical proof systems can be translated for their shifted versions. Finally, it is shown that superpolynomial lower bounds on the size of shifted proofs would separate NP from PSPACE; a connection to lower bounds on circuit complexity is also established.

Download Full-text

Randomized feasible interpolation and monotone circuits with a local oracle

Journal of Mathematical Logic ◽

10.1142/s0219061318500125 ◽

2018 ◽

Vol 18 (02) ◽

pp. 1850012 ◽

Cited By ~ 1

Author(s):

Jan Krajíček

Keyword(s):

Lower Bounds ◽

Cutting Planes ◽

Communication Complexity ◽

Interpolation Theorem ◽

Proof System ◽

Symbolic Logic ◽

Approximate Counting ◽

Small Width ◽

Randomized Protocols ◽

Monotone Circuits

The feasible interpolation theorem for semantic derivations from [J. Krajíček, Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. Symbolic Logic 62(2) (1997) 457–486] allows to derive from some short semantic derivations (e.g. in resolution) of the disjointness of two [Formula: see text] sets [Formula: see text] and [Formula: see text] a small communication protocol (a general dag-like protocol in the sense of Krajíček (1997) computing the Karchmer–Wigderson multi-function [Formula: see text] associated with the sets, and such a protocol further yields a small circuit separating [Formula: see text] from [Formula: see text]. When [Formula: see text] is closed upwards, the protocol computes the monotone Karchmer–Wigderson multi-function [Formula: see text] and the resulting circuit is monotone. Krajíček [Interpolation by a game, Math. Logic Quart. 44(4) (1998) 450–458] extended the feasible interpolation theorem to a larger class of semantic derivations using the notion of a real communication complexity (e.g. to the cutting planes proof system CP). In this paper, we generalize the method to a still larger class of semantic derivations by allowing randomized protocols. We also introduce an extension of the monotone circuit model, monotone circuits with a local oracle (CLOs), that does correspond to communication protocols for [Formula: see text] making errors. The new randomized feasible interpolation thus shows that a short semantic derivation (from a certain class of derivations larger than in the original method) of the disjointness of [Formula: see text], [Formula: see text] closed upwards, yields a small randomized protocol for [Formula: see text] and hence a small monotone CLO separating the two sets. This research is motivated by the open problem to establish a lower bound for proof system [Formula: see text] operating with clauses formed by linear Boolean functions over [Formula: see text]. The new randomized feasible interpolation applies to this proof system and also to (the semantic versions of) cutting planes CP, to small width resolution over CP of Krajíček [Discretely ordered modules as a first-order extension of the cutting planes proof system, J. Symbolic Logic 63(4) (1998) 1582–1596] (system R(CP)) and to random resolution RR of Buss, Kolodziejczyk and Thapen [Fragments of approximate counting, J. Symbolic Logic 79(2) (2014) 496–525]. The method does not yield yet lengths-of-proofs lower bounds; for this it is necessary to establish lower bounds for randomized protocols or for monotone CLOs.

Download Full-text

Lower Bounds on OBDD Proofs with Several Orders

ACM Transactions on Computational Logic ◽

10.1145/3468855 ◽

2021 ◽

Vol 22 (4) ◽

pp. 1-30

Author(s):

Sam Buss ◽

Dmitry Itsykson ◽

Alexander Knop ◽

Artur Riazanov ◽

Dmitry Sokolov

Keyword(s):

Lower Bound ◽

Lower Bounds ◽

Communication Complexity ◽

Multiparty Communication ◽

Constant Degree ◽

Polynomial Size ◽

Explicit Constant ◽

Open Question ◽

System 1 ◽

Exponential Size

This article is motivated by seeking lower bounds on OBDD(∧, w, r) refutations, namely, OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1 - NBP ∧ refutations based on read-once nondeterministic branching programs. These generalize OBDD(∧, r) refutations. There are polynomial size 1 - NBP(∧) refutations of the pigeonhole principle, hence 1-NBP(∧) is strictly stronger than OBDD}(∧, r). There are also formulas that have polynomial size tree-like resolution refutations but require exponential size 1-NBP(∧) refutations. As a corollary, OBDD}(∧, r) does not simulate tree-like resolution, answering a previously open question. The system 1-NBP(∧, ∃) uses projection inferences instead of weakening. 1-NBP(∧, ∃ k is the system restricted to projection on at most k distinct variables. We construct explicit constant degree graphs G n on n vertices and an ε > 0, such that 1-NBP(∧, ∃ ε n ) refutations of the Tseitin formula for G n require exponential size. Second, we study the proof system OBDD}(∧, w, r ℓ ), which allows ℓ different variable orders in a refutation. We prove an exponential lower bound on the complexity of tree-like OBDD(∧, w, r ℓ ) refutations for ℓ = ε log n , where n is the number of variables and ε > 0 is a constant. The lower bound is based on multiparty communication complexity.

Download Full-text