Lower bounds for resolution and cutting plane proofs and monotone computations

1997 ◽  
Vol 62 (3) ◽  
pp. 981-998 ◽  
Author(s):  
Pavel Pudlák

AbstractWe prove an exponential lower bound on the length of cutting plane proofs. The proof uses an extension of a lower bound for monotone circuits to circuits which compute with real numbers and use nondecreasing functions as gates. The latter result is of independent interest, since, in particular, it implies an exponential lower bound for some arithmetic circuits.

1997 ◽  
Vol 62 (3) ◽  
pp. 708-728 ◽  
Author(s):  
Maria Bonet ◽  
Toniann Pitassi ◽  
Ran Raz

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.


1949 ◽  
Vol 14 (1) ◽  
pp. 9-15 ◽  
Author(s):  
Frederic B. Fitch

A demonstrably consistent theory of real numbers has been outlined by the writer in An extension of basic logic1 (hereafter referred to as EBL). This theory deals with non-negative real numbers, but it could be easily modified to deal with negative real numbers also. It was shown that the theory was adequate for proving a form of the fundamental theorem on least upper bounds and greatest lower bounds. More precisely, the following results were obtained in the terminology of EBL: If С is a class of U-reals and is completely represented in Κ′ and if some U-real is an upper bound of С, then there is a U-real which is a least upper bound of С. If D is a class of (U-reals and is completely represented in Κ′, then there is a U-real which is a greatest lower bound of D.


2007 ◽  
Vol 72 (3) ◽  
pp. 941-958 ◽  
Author(s):  
Pavel Hrubeš

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.


2021 ◽  
Author(s):  
Bruno Pasqualotto Cavalar ◽  
Yoshiharu Kohayakawa

Alexander Razborov (1985) developed the approximation method to obtain lower bounds on the size of monotone circuits deciding if a graph contains a clique. Given a "small" circuit, this technique consists in finding a monotone Boolean function which approximates the circuit in a distribution of interest, but makes computation errors in that same distribution. To prove that such a function is indeed a good approximation, Razborov used the sunflower lemma of Erd\H{o}s and Rado (1960). This technique was improved by Alon and Boppana (1987) to show lower bounds for a larger class of monotone computational problems. In that same work, the authors also improved the result of Razborov for the clique problem, using a relaxed variant of sunflowers. More recently, Rossman (2010) developed another variant of sunflowers, now called "robust sunflowers", to obtain lower bounds for the clique problem in random graphs. In the following years, the concept of robust sunflowers found applications in many areas of computational complexity, such as DNF sparsification, randomness extractors and lifting theorems. Even more recent was the breakthrough result of Alweiss, Lovett, Wu and Zhang (2020), which improved Rossman's bound on the size of hypergraphs without robust sunflowers. This result was employed to obtain a significant progress on the sunflower conjecture. In this work, we will show how the recent progress in sunflower theorems can be applied to improve monotone circuit lower bounds. In particular, we will show the best monotone circuit lower bound obtained up to now, breaking a 20-year old record of Harnik and Raz (2000). We will also improve the lower bound of Alon and Boppana for the clique function in a slightly more restricted range of clique sizes. Our exposition is self-contained. These results were obtained in a collaboration with Benjamin Rossman and Mrinal Kumar.


2021 ◽  
Author(s):  
Alexis de Colnet ◽  
Stefan Mengel

Arithmetic circuits (AC) are circuits over the real numbers with 0/1-valued input variables whose gates compute the sum or the product of their inputs. Positive AC – that is, AC representing non-negative functions – subsume many interesting probabilistic models such as probabilistic sentential decision diagram (PSDD) or sum-product network (SPN) on indicator variables. Efficient algorithms for many operations useful in probabilistic reasoning on these models critically depend on imposing structural restrictions to the underlying AC. Generally, adding structural restrictions yields new tractable operations but increases the size of the AC. In this paper we study the relative succinctness of classes of AC with different combinations of common restrictions. Building on existing results for Boolean circuits, we derive an unconditional succinctness map for classes of monotone AC – that is, AC whose constant labels are non-negative reals – respecting relevant combinations of the restrictions we consider. We extend a small part of the map to classes of positive AC. Those are known to generally be exponentially more succinct than their monotone counterparts, but we observe here that for so-called deterministic circuits there is no difference between the monotone and the positive setting which allows us to lift some of our results. We end the paper with some insights on the relative succinctness of positive AC by showing exponential lower bounds on the representations of certain functions in positive AC respecting structured decomposability.


2020 ◽  
Vol 177 (1) ◽  
pp. 69-93
Author(s):  
Purnata Ghosal ◽  
B.V. Raghavendra Rao

We consider the problem of obtaining parameterized lower bounds for the size of arithmetic circuits computing polynomials with the degree of the polynomial as the parameter. We consider the following special classes of multilinear algebraic branching programs: 1) Read Once Oblivious Branching Programs (ROABPs), 2) Strict interval branching programs, 3) Sum of read once formulas with restricted ordering. We obtain parameterized lower bounds (i.e., nΩ(t(k)) lower bound for some function t of k) on the size of the above models computing a multilinear polynomial that can be computed by a depth four circuit of size g(k)nO(1) for some computable function g. Further, we obtain a parameterized separation between ROABPs and read-2 ABPs. This is obtained by constructing a degree k polynomial that can be computed by a read-2 ABP of small size such that the rank of the partial derivative matrix under any partition of the variables is large.


10.37236/1188 ◽  
1994 ◽  
Vol 1 (1) ◽  
Author(s):  
Geoffrey Exoo

For $k \geq 5$, we establish new lower bounds on the Schur numbers $S(k)$ and on the k-color Ramsey numbers of $K_3$.


Algorithms ◽  
2021 ◽  
Vol 14 (6) ◽  
pp. 164
Author(s):  
Tobias Rupp ◽  
Stefan Funke

We prove a Ω(n) lower bound on the query time for contraction hierarchies (CH) as well as hub labels, two popular speed-up techniques for shortest path routing. Our construction is based on a graph family not too far from subgraphs that occur in real-world road networks, in particular, it is planar and has a bounded degree. Additionally, we borrow ideas from our lower bound proof to come up with instance-based lower bounds for concrete road network instances of moderate size, reaching up to 96% of an upper bound given by a constructed CH. For a variant of our instance-based schema applied to some special graph classes, we can even show matching upper and lower bounds.


2021 ◽  
Vol 13 (3) ◽  
pp. 1-21
Author(s):  
Suryajith Chillara

In this article, we are interested in understanding the complexity of computing multilinear polynomials using depth four circuits in which the polynomial computed at every node has a bound on the individual degree of r ≥ 1 with respect to all its variables (referred to as multi- r -ic circuits). The goal of this study is to make progress towards proving superpolynomial lower bounds for general depth four circuits computing multilinear polynomials, by proving better bounds as the value of r increases. Recently, Kayal, Saha and Tavenas (Theory of Computing, 2018) showed that any depth four arithmetic circuit of bounded individual degree r computing an explicit multilinear polynomial on n O (1) variables and degree d must have size at least ( n / r 1.1 ) Ω(√ d / r ) . This bound, however, deteriorates as the value of r increases. It is a natural question to ask if we can prove a bound that does not deteriorate as the value of r increases, or a bound that holds for a larger regime of r . In this article, we prove a lower bound that does not deteriorate with increasing values of r , albeit for a specific instance of d = d ( n ) but for a wider range of r . Formally, for all large enough integers n and a small constant η, we show that there exists an explicit polynomial on n O (1) variables and degree Θ (log 2 n ) such that any depth four circuit of bounded individual degree r ≤ n η must have size at least exp(Ω(log 2 n )). This improvement is obtained by suitably adapting the complexity measure of Kayal et al. (Theory of Computing, 2018). This adaptation of the measure is inspired by the complexity measure used by Kayal et al. (SIAM J. Computing, 2017).


Sign in / Sign up

Export Citation Format

Share Document