Lower bounds for cutting planes proofs with small coefficients

1997 ◽  
Vol 62 (3) ◽  
pp. 708-728 ◽  
Author(s):  
Maria Bonet ◽  
Toniann Pitassi ◽  
Ran Raz
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Cutting Planes ◽  
Communication Complexity ◽  
Proof System ◽  
Small Weight ◽  
Deduction Rule ◽  
Special Case ◽  
Exponential Lower Bound

AbstractWe consider small-weight Cutting Planes (CP*) proofs; that is, Cutting Planes (CP) proofs with coefficients up to Poly(n). We use the well known lower bounds for monotone complexity to prove an exponential lower bound for the length of CP* proofs, for a family of tautologies based on the clique function. Because Resolution is a special case of small-weight CP, our method also gives a new and simpler exponential lower bound for Resolution.We also prove the following two theorems: (1) Tree-like CP* proofs cannot polynomially simulate non-tree-like CP* proofs. (2) Tree-like CP* proofs and Bounded-depth-Frege proofs cannot polynomially simulate each other.Our proofs also work for some generalizations of the CP* proof system. In particular, they work for CP* with a deduction rule, and also for any proof system that allows any formula with small communication complexity, and any set of sound rules of inference.

scholarly journals Randomized feasible interpolation and monotone circuits with a local oracle

2018 ◽  
Vol 18 (02) ◽  
pp. 1850012 ◽  
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.

Lower bounds for modal logics

2007 ◽  
Vol 72 (3) ◽  
pp. 941-958 ◽  
Author(s):  
Pavel Hrubeš
Keyword(s):  
Lower Bound ◽  
Modal Logic ◽  
Lower Bounds ◽  
Modal Logics ◽  
Proof System ◽  
Speed Up ◽  
Exponential Lower Bound

AbstractWe give an exponential lower bound on number of proof-lines in the proof system K of modal logic, i.e., we give an example of K-tautologies ψ1, ψ2, … s.t. every K-proof of ψi must have a number of proof-lines exponential in terms of the size of ψi. The result extends, for the same sequence of K-tautologies, to the systems K4, Gödel–Löb's logic, S andS4. We also determine some speed-up relations between different systems of modal logic on formulas of modal-depth one.

scholarly journals Better protocol for XOR game using communication protocol and nonlocal boxes

2017 ◽  
Vol 17 (15&16) ◽  
pp. 1261-1276
Author(s):  
Ryuhei Mori
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Communication Complexity ◽  
Quantum Communication ◽  
Communication Protocol ◽  
Constant Factor ◽  
Efficient Communication ◽  
Information Causality ◽  
Special Case

Buhrman showed that an efficient communication protocol implies a reliable XOR game protocol. This idea rederives Linial and Shraibman’s lower bound of randomized and quantum communication complexities, which was derived by using factorization norms, with worse constant factor in much more intuitive way. In this work, we improve and generalize Buhrman’s idea, and obtain a class of lower bounds for randomized communication complexity including an exact Linial and Shraibman’s lower bound as a special case. In the proof, we explicitly construct a protocol for XOR game from a randomized communication protocol by using a concept of nonlocal boxes and Paw lowski et al.’s elegant protocol, which was used for showing the violation of information causality in superquantum theories.

Discretely ordered modules as a first-order extension of the cutting planes proof system

1998 ◽  
Vol 63 (4) ◽  
pp. 1582-1596 ◽  
Author(s):  
Jan Krajíček
Keyword(s):  
Lower Bound ◽  
Cutting Planes ◽  
Communication Complexity ◽  
Maximum Size ◽  
Interpolation Theorem ◽  
Proof System ◽  
First Order ◽  
First Order Theory ◽  
Sparse Polynomials ◽  
Order Extension

AbstractWe define a first-order extension LK(CP) of the cutting planes proof system CP as the first-order sequent calculus LK whose atomic formulas are CP-inequalities ∑i ai · xi ≥ b (xi's variables, ai's and b constants). We prove an interpolation theorem for LK(CP) yielding as a corollary a conditional lower bound for LK(CP)-proofs. For a subsystem R(CP) of LK(CP), essentially resolution working with clauses formed by CP-inequalities, we prove a monotone interpolation theorem obtaining thus an unconditional lower bound (depending on the maximum size of coefficients in proofs and on the maximum number of CP-inequalities in clauses). We also give an interpolation theorem for polynomial calculus working with sparse polynomials.The proof relies on a universal interpolation theorem for semantic derivations [16, Theorem 5.1].LK(CP) can be viewed as a two-sorted first-order theory of Z considered itself as a discretely ordered Z-module. One sort of variables are module elements, another sort are scalars. The quantification is allowed only over the former sort. We shall give a construction of a theory LK(M) for any discretely ordered module M (e.g., LK(Z) extends LK(CP)). The interpolation theorem generalizes to these theories obtained from discretely ordered Z-modules. We shall also discuss a connection to quantifier elimination for such theories.We formulate a communication complexity problem whose (suitable) solution would allow to improve the monotone interpolation theorem and the lower bound for R(CP).

Lower Bounds on OBDD Proofs with Several Orders

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.

SIMULATIONS OF UNARY ONE-WAY MULTI-HEAD FINITE AUTOMATA

2014 ◽  
Vol 25 (07) ◽  
pp. 877-896 ◽  
Author(s):  
MARTIN KUTRIB ◽  
ANDREAS MALCHER ◽  
MATTHIAS WENDLANDT
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Finite Automaton ◽  
Finite Automata ◽  
Upper And Lower Bounds ◽  
Unary Languages ◽  
Order Of Magnitude ◽  
Simulation Results ◽  
Special Case ◽  
Nondeterministic Finite Automaton

We investigate the descriptional complexity of deterministic one-way multi-head finite automata accepting unary languages. It is known that in this case the languages accepted are regular. Thus, we study the increase of the number of states when an n-state k-head finite automaton is simulated by a classical (one-head) deterministic or nondeterministic finite automaton. In the former case upper and lower bounds that are tight in the order of magnitude are shown. For the latter case we obtain an upper bound of O(n2k) and a lower bound of Ω(nk) states. We investigate also the costs for the conversion of one-head nondeterministic finite automata to deterministic k-head finite automata, that is, we trade nondeterminism for heads. In addition, we study how the conversion costs vary in the special case of finite and, in particular, of singleton unary lanuages. Finally, as an application of the simulation results, we show that decidability problems for unary deterministic k-head finite automata such as emptiness or equivalence are LOGSPACE-complete.

scholarly journals Augmenting the Power of (Partial) MaxSat Resolution with Extension

2020 ◽  
Vol 34 (02) ◽  
pp. 1561-1568 ◽  
Author(s):  
Javier Larrosa ◽  
Emma Rollon
Keyword(s):  
Lower Bound ◽  
Objective Function ◽  
Lower Bounds ◽  
Polynomial Time ◽  
Proof System ◽  
Extension Rule ◽  
Resolution Proof

The refutation power of SAT and MaxSAT resolution is challenged by problems like the soft and hard Pigeon Hole Problem PHP for which short refutations do not exist. In this paper we augment the MaxSAT resolution proof system with an extension rule. The new proof system MaxResE is sound and complete, and more powerful than plain MaxSAT resolution, since it can refute the soft and hard PHP in polynomial time. We show that MaxResE refutations actually subtract lower bounds from the objective function encoded by the formulas. The resulting formula is the residual after the lower bound extraction. We experimentally show that the residual of the soft PHP (once its necessary cost of 1 has been efficiently subtracted with MaxResE) is a concise, easy to solve, satisfiable problem.

scholarly journals Lower Bounds for Dynamic Algebraic Problems

1998 ◽  
Vol 5 (11) ◽  
Author(s):  
Gudmund Skovbjerg Frandsen ◽  
Johan P. Hansen ◽  
Peter Bro Miltersen
Keyword(s):  
Fourier Transform ◽  
Lower Bound ◽  
Lower Bounds ◽  
Communication Complexity ◽  
Symmetric Functions ◽  
Matrix Multiplication ◽  
Worst Case ◽  
Dynamic Matrix ◽  
Wide Range ◽  
On Line

We consider dynamic evaluation of algebraic functions (matrix multiplication, determinant, convolution, Fourier transform, etc.) in the model of Reif and Tate; i.e., if f(x1, . . . , xn) = (y1, . . . , ym) is an algebraic problem, we consider serving on-line requests of the form "change input xi to value v" or "what is the value of output yi?". We present techniques for showing lower bounds on the worst case time complexity per operation for such problems. The first gives lower bounds in a wide range of rather powerful models (for instance history dependent<br />algebraic computation trees over any infinite subset of a field, the integer RAM, and the generalized real RAM model of Ben-Amram and Galil). Using this technique, we show optimal  Omega(n) bounds for dynamic matrix-vector product, dynamic matrix multiplication and dynamic discriminant and an <br />Omega(sqrt(n)) lower bound for dynamic polynomial multiplication (convolution), providing a good match with Reif and<br />Tate's O(sqrt(n log n)) upper bound. We also show linear lower bounds for dynamic determinant, matrix adjoint and matrix inverse and an Omega(sqrt(n)) lower bound for the elementary symmetric functions. The second technique is the communication complexity technique of Miltersen, Nisan, Safra, and Wigderson which we apply to the setting<br />of dynamic algebraic problems, obtaining similar lower bounds in the word RAM model. The third technique gives lower bounds in the weaker straight line program model. Using this technique, we show an ((log n)2= log log n) lower bound for dynamic discrete Fourier transform. Technical ingredients of our techniques are the incompressibility technique of Ben-Amram and Galil and the lower bound for depth-two superconcentrators of Radhakrishnan and Ta-Shma. The incompressibility technique is extended to arithmetic computation in arbitrary fields.

Quantum uncertainty relations of Tsallis relative $\alpha$ entropy coherence baed on MUBs

2021 ◽  
Author(s):  
ZHANG Fu Gang
Keyword(s):  
Lower Bound ◽  
Positive Integer ◽  
Lower Bounds ◽  
Upper And Lower Bounds ◽  
Mutually Unbiased Bases ◽  
Uncertainty Relations ◽  
Quantum Uncertainty ◽  
Single Qubit ◽  
Qubit System ◽  
Special Case

Abstract In this paper, we discuss quantum uncertainty relations of Tsallis relative $\alpha$ entropy coherence for a single qubit system based on three mutually unbiased bases. For $\alpha\in[\frac{1}{2},1)\cup(1,2]$, the upper and lower bounds of sums of coherence are obtained. However, the above results cannot be verified directly for any $\alpha\in(0,\frac{1}{2})$. Hence, we only consider the special case of $\alpha=\frac{1}{n+1}$, where $n$ is a positive integer, and we obtain the upper and lower bounds. By comparing the upper and lower bounds, we find that the upper bound is equal to the lower bound for the special $\alpha=\frac{1}{2}$, and the differences between the upper and the lower bounds will increase as $\alpha$ increases. Furthermore, we discuss the tendency of the sum of coherence, and find that it has the same tendency with respect to the different $\theta$ or $\varphi$, which is opposite to the uncertainty relations based on the R\'{e}nyi entropy and Tsallis entropy.

scholarly journals On the Distributed Complexity of Large-Scale Graph Computations

2021 ◽  
Vol 8 (2) ◽  
pp. 1-28
Author(s):  
Gopal Pandurangan ◽  
Peter Robinson ◽  
Michele Scquizzato
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Distributed Algorithm ◽  
Message Passing ◽  
Large Scale ◽  
Communication Complexity ◽  
Minimal Amount ◽  
Theoretic Approach ◽  
Graph Problems ◽  
Round Complexity

Motivated by the increasing need to understand the distributed algorithmic foundations of large-scale graph computations, we study some fundamental graph problems in a message-passing model for distributed computing where k ≥ 2 machines jointly perform computations on graphs with n nodes (typically, n >> k). The input graph is assumed to be initially randomly partitioned among the k machines, a common implementation in many real-world systems. Communication is point-to-point, and the goal is to minimize the number of communication rounds of the computation. Our main contribution is the General Lower Bound Theorem , a theorem that can be used to show non-trivial lower bounds on the round complexity of distributed large-scale data computations. This result is established via an information-theoretic approach that relates the round complexity to the minimal amount of information required by machines to solve the problem. Our approach is generic, and this theorem can be used in a “cookbook” fashion to show distributed lower bounds for several problems, including non-graph problems. We present two applications by showing (almost) tight lower bounds on the round complexity of two fundamental graph problems, namely, PageRank computation and triangle enumeration . These applications show that our approach can yield lower bounds for problems where the application of communication complexity techniques seems not obvious or gives weak bounds, including and especially under a stochastic partition of the input. We then present distributed algorithms for PageRank and triangle enumeration with a round complexity that (almost) matches the respective lower bounds; these algorithms exhibit a round complexity that scales superlinearly in k , improving significantly over previous results [Klauck et al., SODA 2015]. Specifically, we show the following results: PageRank: We show a lower bound of Ὼ(n/k 2 ) rounds and present a distributed algorithm that computes an approximation of the PageRank of all the nodes of a graph in Õ(n/k 2 ) rounds. Triangle enumeration: We show that there exist graphs with m edges where any distributed algorithm requires Ὼ(m/k 5/3 ) rounds. This result also implies the first non-trivial lower bound of Ὼ(n 1/3 ) rounds for the congested clique model, which is tight up to logarithmic factors. We then present a distributed algorithm that enumerates all the triangles of a graph in Õ(m/k 5/3 + n/k 4/3 ) rounds.

Sign in / Sign up

Export Citation Format

Share Document