Depth-3 circuit lower bounds and k-SAT algorithms are intimately related; the state-of-the-art Σ^k_3-circuit lower bound (Or-And-Or circuits with bottom fan-in at most k) and the k-SAT algorithm of Paturi, Pudlák, Saks, and Zane (J. ACM'05) are based on the same combinatorial theorem regarding k-CNFs. In this paper we define a problem which reveals new interactions between the two, and suggests a concrete approach to significantly stronger circuit lower bounds and improved k-SAT algorithms. For a natural number k and a parameter t, we consider the Enum(k, t) problem defined as follows: given an n-variable k-CNF and an initial assignment α, output all satisfying assignments at Hamming distance t(n) of α, assuming that there are no satisfying assignments of Hamming distance less than t(n) of α. We observe that an upper bound b(n, k, t) on the complexity of Enum(k, t) simultaneously implies depth-3 circuit lower bounds and k-SAT algorithms: - Depth-3 circuits: Any Σ^k_3 circuit computing the Majority function has size at least binom(n,n/2)/b(n, k, n/2). - k-SAT: There exists an algorithm solving k-SAT in time O(∑_{t=1}^{n/2}b(n, k, t)). A simple construction shows that b(n, k, n/2) ≥ 2^{(1 - O(log(k)/k))n}. Thus, matching upper bounds for b(n, k, n/2) would imply a Σ^k_3-circuit lower bound of 2^Ω(log(k)n/k) and a k-SAT upper bound of 2^{(1 - Ω(log(k)/k))n}. The former yields an unrestricted depth-3 lower bound of 2^ω(√n) solving a long standing open problem, and the latter breaks the Super Strong Exponential Time Hypothesis. In this paper, we propose a randomized algorithm for Enum(k, t) and introduce new ideas to analyze it. We demonstrate the power of our ideas by considering the first non-trivial instance of the problem, i.e., Enum(3, n/2). We show that the expected running time of our algorithm is 1.598ⁿ, substantially improving on the trivial bound of 3^{n/2} ≃ 1.732ⁿ. This already improves Σ^3_3 lower bounds for Majority function to 1.251ⁿ. The previous bound was 1.154ⁿ which follows from the work of Håstad, Jukna, and Pudlák (Comput. Complex.'95). By restricting ourselves to monotone CNFs, Enum(k, t) immediately becomes a hypergraph Turán problem. Therefore our techniques might be of independent interest in extremal combinatorics.

A natural model of read-once linear branching programs is a branching program where queries are $\mathbb{F}_2$ linear forms, and along each path, the queries are linearly independent. We consider two restrictions of this model, which we call weakly and strongly read-once, both generalizing standard read-once branching programs and parity decision trees. Our main results are as follows. - Average-case complexity. We define a pseudo-random class of functions which we call directional affine extractors, and show that these functions are hard on average for the strongly read-once model. We then present an explicit construction of such function with good parameters. This strengthens the result of Cohen and Shinkar (ITCS'16) who gave such average-case hardness for parity decision trees. Directional affine extractors are stronger than the more familiar class of affine extractors. Given the significance of these functions, we expect that our new class of functions might be of independent interest. - Proof complexity. We also consider the proof system $\text{Res}[\oplus]$ which is an extension of resolution with linear queries. A refutation of a CNF in this proof system naturally defines a linear branching program solving the corresponding search problem. Conversely, we show that a weakly read-once linear BP solving the search problem can be converted to a $\text{Res}[\oplus]$ refutation with constant blow up.

We investigate the algorithmic properties of circuits of bounded treewidth. Here the treewidth of a circuit C is defined as the treewidth of the underlying undirected graph of C, after the vertices corresponding to input gates have been removed. Thus, boolean formulae correspond to circuits of treewidth 1. Our first main result is an algorithm for counting the number of satisfying assignments of circuits with n input gates, treewidth ω, and at most s · n gates. The running time of our algorithm is , which for formulae instantiates to 2n(1–1/O(s)). This is the first algorithm to achieve exponential speedup over brute force for the satisfiability of linear size circuits with treewidth bounded by a constant greater than 1. For treewidth 1, i.e., boolean formulae, our algorithm significantly outperforms the previously fastest 2n(1-1/O(s2)) time satisfiability algorithm by Santhanam [32]. Our second main result is an algorithm for True Quantified Boolean Circuit Satisfiability for circuits of treewidth ω, in which every input gate has fanout at most s. The running time of our algorithm is . Our algorithm is the first to achieve exponential speed-up over brute force for such circuits. Indeed, even for quantified boolean formulae where every variable appears at most s times, the previously best known algorithm by Santhanam [32] has running time 2n(1–1/O(f(s)log n)). Utilizing the structural properties of low treewidth circuits which helped us obtain improved exponential-time algorithms for satisfiability, we also show that the number of wires of any constant treewidth circuit that computes the majority function must be super-linear.

We introduce the notion of monotone linear-programming circuits (MLP circuits), a model of computation for partial Boolean functions. Using this model, we prove the following results. 1. MLP circuits are superpolynomially stronger than monotone Boolean circuits. 2. MLP circuits are exponentially stronger than monotone span programs. 3. MLP circuits can be used to provide monotone feasibility interpolation theorems for Lovasz-Schrijver proof systems, and for mixed Lovasz-Schrijver proof systems. 4. The Lovasz-Schrijver proof system cannot be polynomially simulated by the cutting planes proof system. This is the first result showing a separation between these two proof systems. Finally, we discuss connections between the problem of proving lower bounds on the size of MLPs and the problem of proving lower bounds on extended formulations of polytopes.

We study the random resolution refutation system definedin [Buss et al. 2014]. This attempts to capture the notion of a resolution refutation that may make mistakes but is correct most of the time. By proving the equivalence of several different definitions, we show that this concept is robust. On the other hand, if P does not equal NP, then random resolution cannot be polynomially simulated by any proof system in which correctness of proofs is checkable in polynomial time. We prove several upper and lower bounds on the width and size of random resolution refutations of explicit and random unsatisfiable CNF formulas. Our main result is a separation between polylogarithmic width random resolution and quasipolynomial size resolution, which solves the problem stated in [Buss et al. 2014]. We also prove exponential size lower bounds on random resolution refutations of the pigeonhole principle CNFs, and of a family of CNFs which have polynomial size refutations in constant depth Frege.

We prove new lower bounds on the sizes of proofs in the Cutting Plane proof system, using a concept that we call unsatisfiability certificate. This approach is, essentially, equivalent to the well-known feasible interpolation method, but is applicable to CNF formulas that do not seem suitable for interpolation. Specifically, we prove exponential lower bounds for random k-CNFs, where k is the logarithm of the number of variables, and for the Weak Bit Pigeon Hole Principle. Furthermore, we prove a monotone variant of a hypothesis of Feige [12]. We give a superpolynomial lower bound on monotone real circuits that approximately decide the satisfiability of k-CNFs, where k = ω(1). For k ≈ log n, the lower bound is exponential.

We construct uniquely satisfiable $k$-CNF formulas that are hard for the algorithm PPSZ. Firstly, we construct graph-instances on which "weak PPSZ" has savings of at most $(2 + ε) / k$; the saving of an algorithm on an input formula with $n$ variables is the largest $γ$ such that the algorithm succeeds (i.e. finds a satisfying assignment) with probability at least $2^{ - (1 - γ) n}$. Since PPSZ (both weak and strong) is known to have savings of at least $\frac{π^2 + o(1)}{6k}$, this is optimal up to the constant factor. In particular, for $k=3$, our upper bound is $2^{0.333\dots n}$, which is fairly close to the lower bound $2^{0.386\dots n}$ of Hertli [SIAM J. Comput.'14]. We also construct instances based on linear systems over $\mathbb{F}_2$ for which strong PPSZ has savings of at most $O\left(\frac{\log(k)}{k}\right)$. This is only a $\log(k)$ factor away from the optimal bound. Our constructions improve previous savings upper bound of $O\left(\frac{\log^2(k)}{k}\right)$ due to Chen et al. [SODA'13].

We study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of linear inequalities that need to be kept on a blackboard while verifying it. We show that any unsatisfiable set of linear inequalities has a cutting planes refutation in space five. This is in contrast to the weaker resolution proof system, for which the analogous space measure has been well-studied and many optimal linear lower bounds are known. Motivated by this result we consider a natural restriction of cutting planes, in which all coefficients have size bounded by a constant. We show that there is a CNF which requires super-constant space to refute in this system. The system nevertheless already has an exponential speed-up over resolution with respect to size, and we additionally show that it is stronger than resolution with respect to space, by constructing constant-space cutting planes proofs, with coefficients bounded by two, of the pigeonhole principle. We also consider variable instance space for cutting planes, where we count the number of instances of variables on the blackboard, and total space, where we count the total number of symbols.

We introduce a new concept, which we call partition expanders. The basic idea is to study quantitative properties of graphs in a slightly different way than it is in the standard definition of expanders. While in the definition of expanders it is required that the number of edges between any pair of sufficiently large sets is close to the expected number, we consider partitions and require this condition only for most of the pairs of blocks. As a result, the blocks can be substantially smaller. We show that for some range of parameters, to be a partition expander a random graph needs exponentially smaller degree than any expander would require in order to achieve similar expanding properties. We apply the concept of partition expanders in communication complexity. First, we give a PRG for the SMP model of the optimal seed length, n+O(log(k)). Second, we compare the model of SMP to that of Simultaneous Two-Way Communication, and give a new separation that is stronger both qualitatively and quantitatively than the previously known ones.

A propositional proof system is weakly automatizable if there is a polynomial time algorithm that separates satisfiable formulas from formulas that have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time. We give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to mean payoff and simple stochastic games. We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy. Our main technique is to show that a suitable weak bounded arithmetic theory proves that both players in a game cannot simultaneously have a winning strategy, and then to translate this proof into propositional form.

We bound the minimum number$w$of wires needed to compute any (asymptotically good) error-correcting code$C:\{0,1\}^{\Omega (n)}\to\{0,1\}^{n}$with minimum distance$\Omega (n)$, using unbounded fan-in circuits of depth$d$with arbitrary gates. Our main results are: 1) if$d=2$, then$w=\Theta (n ({\lg n/\lg\lg n})^{2})$; 2) if$d=3$, then$w=\Theta (n\lg\lg n)$; 3) if$d=2k$or$d=2k+1$for some integer$k\geq 2$, then$w=\Theta (n\lambda_{k}(n))$, where$\lambda_{1}(n)=\lceil\lg n\rceil$,$\lambda_{i+1}(n)=\lambda_{i}^{\ast}(n)$, and the$\ast$operation gives how many times one has to iterate the function$\lambda_{i}$to reach a value at most 1 from the argument$n$; and 4) if$d=\lg^{\ast}n$, then$w=O(n)$. For depth$d=2$, our$\Omega (n ({\lg n/\lg\lg n})^{2})$lower bound gives the largest known lower bound for computing any linear map. The upper bounds imply that a (necessarily dense) generator matrix for our code can be written as the product of two sparse matrices. Using known techniques, we also obtain similar (but not tight) bounds for computing pairwise-independent hash functions. Our lower bounds are based on a superconcentrator-like condition that the graphs of circuits computing good codes must satisfy. This condition is provably intermediate between superconcentrators and their weakenings considered before.

We bound the minimum number w of wires needed to compute any (asymptotically good) error-correcting code C:{0,1}Ω(n) -> {0,1}n with minimum distance Ω(n), using unbounded fan-in circuits of depth d with arbitrary gates. Our main results are: (1) If d=2 then w = Θ(n ({log n/ log log n})2). (2) If d=3 then w = Θ(n lg lg n). (3) If d=2k or d=2k+1 for some integer k ≥ 2 then w = Θ(n λk(n)), where λ1(n)=⌈ log n⌉, λi+1(n)= λi*(n), and the * operation gives how many times one has to iterate the function λi to reach a value at most 1 from the argument n. (4) If d=log* n then w=O(n).

We prove that the pseudorandom generator introduced by Impagliazzo Nisan and Wigderson with proper choice of parameters fools group products of a given finite group. The seed length is logarithmic in the size of the inputs.

This paper describes a project that aims at showing that propositional proofs of certain tautologies in weak proof system give upper bounds on the computational complexity of functions associated with the tautologies. Such bounds can potentially be used to prove (conditional or unconditional) lower bounds on the lengths of proofs of these tautologies and show separations of some weak proof systems. The prototype are the results showing the feasible interpolation property for resolution. In order to prove similar results for systems stronger than resolution one needs to define suitable generalizations of boolean circuits. We will survey the known results concerning this project and sketch in which direction we want to generalize them.

In this paper, we are concerned with the exponential complexity of the Circuit Satisfiability (CktSat) problem and more generally with the exponential complexity of NP-complete problems. Over the past 15 years or so, researchers have obtained a number of exponential-time algorithms with improved running times for exactly solving a variety of NP-complete problems. The improvements are typically in the form of better exponents compared to exhaustive search. Our goal is to develop techniques to prove specific lower bounds on the exponents under plausible complexity assumptions. We consider natural, though restricted, algorithmic paradigms and prove upper bounds on the success probability. Our approach has the advantage of clarifying the relative power of various algorithmic paradigms. Our main technique is a success probability amplification technique, called the Exponential Amplification Lemma, which shows that for any f(n,m)-size bounded probabilistic circuit family A that decides CktSat with success probability at least 2-α n for α<1 on inputs which are circuits of size m with n variables, there is another probabilistic circuit family B that decides CktSat with size roughly f(α n, f(n,m)) and success probability about 2-α2 n > 2-α n.

We give the first exponential separation between quantum and classical multi-party communication complexity in the (non-interactive) one-way and simultaneous message passing settings.

Abstract We consider the problem whether the theorems of the fragments form a strictly increasing hierarchy. We shall show a link to some results about the lengths of proofs in predicate logic that supports the conjecture that the hierarchy is strictly increasing.

Godel was born 100 years ago in this country. It is a good opportunity to commemorate this anniversary by a lecture about his influence on computational complexity.

Let CCo(n)[m] be the class of circuits that have size o(n) and in which all gates are MOD[m] gates. We show that CC [m] circuits cannot compute MODqin sub-linear size when m, q > 1 are co-prime integers. No non-trivial lower bounds were known before on the size of CC [m] circuits of constant depth for computing MODq. On the other hand, our results show circuits of type MAJ o CCo(n)[m] need exponential size to compute MODq. Using Bourgain's recent breakthrough result on estimates of exponential sums, we extend our bound to the case where small fan-in AND gates are allowed at the bottom of such circuits i.e. circuits of type MAJ o CC[m] o ANDepsiv log n, where epsiv > 0 is a sufficiently small constant. CC [m] circuits of constant depth need superlinear number of wires to compute both the AND and MODqfunctions. To prove this, we show that any circuit computing such functions has a certain connectivity property that is similar to that of superconcentration. We show a superlinear lower bound on the number of edges of such graphs extending results on superconcentrators

We develop a new method to analyze the flow of communication in constant-depth circuits. This point of view allows usto prove new lower bounds on the number of wires required to recognize certain languages. We are able to provide explicit languages that can be recognized by AC0 circuits with O(n) gates but not with O(n) wires, and similarly for ACC0 circuits. We are also able to characterize exactly the regular languages that can be recognized with O(n) wires, both in AC0 and ACC0 framework.

We propose and analyze a simple new randomized algorithm, called ResolveSat, for finding satisfying assignments of Boolean formulas in conjunctive normal form. The algorithm consists of two stages: a preprocessing stage in which resolution is applied to enlarge the set of clauses of the formula, followed by a search stage that uses a simple randomized greedy procedure to look for a satisfying assignment. Currently, this is the fastest known probabilistic algorithm for k -CNF satisfiability for k ≥ 4 (with a running time of O (2 0.5625 n ) for 4-CNF). In addition, it is the fastest known probabilistic algorithm for k -CNF, k ≥ 3, that have at most one satisfying assignment (unique k -SAT) (with a running time O (2 (2 ln 2 − 1) n + o ( n ) ) = O (2 0.386 … n ) in the case of 3-CNF). The analysis of the algorithm also gives an upper bound on the number of the codewords of a code defined by a k -CNF. This is applied to prove a lower bounds on depth 3 circuits accepting codes with nonconstant distance. In particular we prove a lower bound Ω(2 1.282…√>i /i< ) for an explicitly given Boolean function of n variables. This is the first such lower bound that is asymptotically bigger than 2 √>i /i< + o (√>i /i<) .

Abstract We consider combinatorial principles based on playing several two person games simultaneously. We call strategies for playing two or more games simultaneously parallel. The principles are easy consequences of the determinacy of games, in particular they are true for all finite games. We shall show that the principles fail for infinite games. The statements of these principles are of lower logical complexity than the sentence expressing the determinacy of games, therefore, they can be studied in weak axiomatic systems for arithmetic (Bounded Arithmetic). We pose several open problems about the provability of these statements in Bounded Arithmetic and related computational problems.

We show that an LK proof of size m of a monotone sequent (a sequent that contains only formulas in the basis /spl and/, V) can be turned into a proof containing only monotone formulas of size m/sup O(log m)/ and with the number of proof lines polynomial in m. Also we show that some interesting special cases, namely the functional and the onto versions of PHP and a version of the matching principle, have polynomial size monotone proofs.

We propose and analyze a simple new algorithm for finding satisfying assignments of Boolean formulae in conjunctive normal form. The algorithm, ResolveSat, is a randomized variant of the DDL procedure by M. Davis et al. (1962) or Davis-Putnam procedure. Rather than applying the DLL procedure to the input formula F, however; ResolveSat enlarges F by adding additional clauses using limited resolution before performing DLL. The basic idea behind our analysis is the same as by R. Paturi (1997): a critical clause for a variable at a satisfying assignment gives rise to a unit clause in the DLL procedure with sufficiently high probability, thus increasing the probability of finding a satisfying assignment. In the current paper, we analyze the effect of multiple critical clauses (obtained through resolution) in producing unit clauses. We show that, for each k, the running time of ResolveSat on a k-CNF formula is significantly better than 2/sup n/, even in the worst case. In particular we show that the algorithm finds a satisfying assignment of a general 3-CNF in time O(2/sup .446n/) with high probability; where the best previous algorithm has running time O(2/sup .582n/). We obtain a better upper bound of O(2/sup (2ln2-1)/n+0(n))=O(2/sup 0.387n/) for 3-CNF that have at most one satisfying assignment (unique k-SAT). For each k, the bounds for general k-CNF are the best known for the worst-case complexity of finding a satisfying solution for k-SAT, the idea of succinctly encoding satisfying solutions can be applied to obtain lower bounds on circuit site. Here, we exhibit a function f such that any depth-3 AND-OR circuit with bottom fan-in bounded by k requires /spl Omega/(2(c/sub k/n/k)) gates (with c/sub k/>1). This is the first such lower bound with c/sub k/>1.

We present and analyze two simple algorithms for finding satisfying assignments of /spl kappa/-CNFs (Boolean formulae in conjunctive normal form with at most /spl kappa/ literals per clause). The first is a randomized algorithm which, with probability approaching 1, finds a satisfying assignment of a satisfiable /spl kappa/-CNF formula F in time O(n/sup 2/|F|2/sup n-n//spl kappa//). The second algorithm is deterministic, and its running time approaches 2/sup n-n/2/spl kappa// for large n and /spl kappa/. The randomized algorithm is the best known algorithm for /spl kappa/>3; the deterministic algorithm is the best known deterministic algorithm for /spl kappa/>4. We also show an /spl Omega/(n/sup 1/4/2/sup /spl radic/n/) lower bound on the size of depth 3 circuits of AND and OR gates computing the parity function. This bound is tight up to a constant factor. The key idea used in these upper and lower bounds is what we call the Satisfiability Coding Lemma. This basic lemma shows how to encode satisfying solutions of a /spl kappa/-CNF succinctly.

Abstract We 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.

We investigate two methods for proving lower bounds on the size of small-depth circuits, namely the approaches based on multiparty communication games and algebraic characterizations extending the concepts of the tensor rank and rigidity of matrices. Our methods are combinatorial, but we think that our main contribution concerns the algebraic concepts used in this area (tensor ranks and rigidity). Our main results are following. (i) An $o(n)$-bit protocol for a communication game for computing shifts, which also gives an upper bound of $o(n^2)$ on the contact rank of the tensor of multiplication of polynomials; this disproves some earlier conjectures. A related probabilistic construction gives an $o(n)$ upper bound for computing all permutations and an $O(n\log\log n)$ upper bound on the communication complexity of pointer jumping with permutations. (ii) A lower bound on certain restricted circuits of depth 2 which are related to the problem of proving a superlinear lower bound on the size of logarithmic-depth circuits; this bound has interpretations both as a lower bound on the rigidity of the tensor of multiplication of polynomials and as a lower bound on the communication needed to compute the shift function in a restricted model. (iii) An upper bound on Boolean circuits of depth 2 for computing shifts and, more generally, all permutations; this shows that such circuits are more efficient than the model based on sending bits along vertex-disjoint paths.

We investigate the complexity of Boolean functions f with respect to realizations by real polynomials p (voting polynomials) in the sense that the sign of p(x) determines the value f(x). Considerable research has been done on determining the minimal degree needed for realizing or approximating particular functions. In this paper we focus our interest on estimating the minimal number of monomials, i.e. the length of realizing polynomials. Our main observation is that, in contrast to the degree, the minimal length essentially depends on whether we realize f over the domain.

The weak form of the Hilbert's Nullstellensatz says that a system of algebraic equations over a field, Q/sub i/(x~)=0, does not have a solution in the algebraic closure iff 1 is in the ideal generated by the polynomials Q/sub i/(x~). We shall prove a lower bound on the degrees of polynomials P/sub i/(x~) such that /spl Sigma//sub i/ P/sub i/(x~)Q/sub i/(x~)=1. This result has the following application. The modular counting principle states that no finite set whose cardinality is not divisible by q can be partitioned into q-element classes. For each fixed cardinality N, this principle can be expressed as a propositional formula Count/sub q//sup N/. Ajtai (1988) proved recently that, whenever p, q are two different primes, the propositional formulas Count/sub q//sup qn+1/ do not have polynomial size, constant-depth Frege proofs from instances of Count/sub p//sup m/, m/spl ne/0 (mod p). We give a new proof of this theorem based on the lower bound for the Hilbert's Nullstellensatz. Furthermore our technique enables us to extend the independence results for counting principles to composite numbers p and q. This results in an exact characterization of when Count/sub q/ can be proven efficiently from Count/sub p/, for all p and q.>

w"e investigate the computational power of depth two circuits consisting of iVfOLY-gates at the bottom and a threshold gate at the top (for short, threshold-MODr

We present a top-down lower bound method for depth 3 AND-OR-NOT circuits which is simpler than the previous methods and in some cases gives better lower bounds. In particular we prove that depth 3 AND-OR-NOT circuits that compute PARITY resp. MAJORITY require size at least 2/sup 0.618/ .../spl radic/n/ resp. 2/sup 0.849/.../spl radic/n/. This is the first simple proof of a strong lower bound by a top-down argument for non-monotone circuits.>

Article Free Access Share on Modified ranks of tensors and the size of circuits Authors: P. Pudlák View Profile , V. Rödl View Profile Authors Info & Claims STOC '93: Proceedings of the twenty-fifth annual ACM symposium on Theory of ComputingJune 1993 Pages 523–531https://doi.org/10.1145/167088.167228Published:01 June 1993Publication History 16citation338DownloadsMetricsTotal Citations16Total Downloads338Last 12 Months11Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

In this paper we prove an exponential lower bound on the size of bounded-depth Frege proofs for the pigeonhole principle (PHP).We also obtain an ~(log log rz)depth lower bound for any polynomial-sized Frege proof of the pigeonhole principle.Our theorem nearly completes the search for the exact complexity of the PHP, as Sam Buss has constructed polynomial-size, log ndepth Frege proofs for the PHP.The main lemma in our proof can be viewed as a general H&.stad-style Switching Lemma for restrictions that are partial matchings.Our lower bounds for the pigeonhole principle improve on previous superpolynomial lower bounds.

Abstract We consider the problem about the length of proofs of the sentences saying that there is no proof of contradiction in S whose length is < n. We show the relation of this problem to some problems about propositional proof systems.

We examine a powerful model of parallel computation: polynomial size threshold circuits of bounded depth (the gates compute threshold functions with polynomial weights). Lower bounds are given to separate polynomial size threshold circuits of depth 2 from polynomial size threshold circuits of depth 3, and from probabilistic polynomial size threshold circuits of depth 2. We also consider circuits of unreliable threshold gates, circuits of imprecise threshold gates and threshold quantifiers.

The first result concerns branching programs having width (log n) °{*).We give an fl(n log n~ log log n) lower bound for the size of such branching programs computing almost any symmetric Boolean fnnction and in particular the following explicit fnnction: "the sum of the input variables is a quadratic residue mod p" where p is any given prime between n 1/4 and n 1/3.This is a strengthening of previous nonlinear lower bounds obtained by Chandra, Furst, Lipton and by Pudlgk.We mention that by iterating our method the result can be further strengthened to lfl(nlog n).The second result is a C" lower bound for read-onceonly branching programs computing an explicit Boolean function.For n = (~), the function computes the parity of the number of triangles in a graph on v vertices.This improves previous exp(cx/n ) lower bounds for other graph functions by Wegener and Z£k.The result implies a linear lower bound for the space complexity of this Boolean function on "eraser machines", i.e. machines that erase each input bit immediately after having read it.

Interpretability in reflexive theories, especially in PA, has been studied in many papers; see e.g. [3], [6], [7], [10], [11], [15], [26]. It has been shown that reflexive theories exhibit many nice properties, e.g. (1) if T, S are recursively enumerable reflexive, then T is interpretable in S iff every Π1 sentence provable in T is provable in S; and (2) if S is reflexive, T is recursively enumerable and locally interpretable in S (i.e. every finite part of T is interpretable in S), then T is globally interpretable in S (Orey's theorem, cf. [3]). In this paper we want to study such statements for nonreflexive theories, especially for finitely axiomatizable theories (which are never reflexive). These theories behave differently, although they may be quite close to reflexive theories, as e.g. GB to ZF. An important fact is that in such theories one can define proper cuts. By a cut we mean a formula with one free variable which defines a nonempty initial segment of natural numbers closed under the successor function. The importance of cuts for interpretations in GB was realized already by Vopěnka and Hájek in [30]. Pioneering work was done by Solovay in [24]. There he developed the method of “shortening of cuts”. Using this method it is possible to replace any cut by a cut which is contained in it and has some desirable additional properties; in particular it can be closed under + and ·. This introduces ambiguity in the concept of arithmetic in theories which admit proper cuts, namely, which cut (closed under + and ·) should be called the arithmetic of the theory? Cuts played the crucial role also in [20].

Classical set theory is considered as the framework of contemporary mathematics. But there are aspects of our understanding of the real world about what it is not clear that they are described in Cantor's set theory in the best possible way. For example the formalization of some intuitive concepts such as the description of vague properties (which led to the theory of fuzzy sets) and the interpretation of the notion of infinitely small quantities (modelled by nonstandard models) is not quite simple in the classical set theory. Therefore it is natural to look for an alternative to Cantor's set theory which would enable us to formalize these considerations more naturally and which would be a sufficiently strong framework for mathematics at the same time. The alternative set theory which was created by P. Vopěnka (cf. [V]) is an attempt to construct a theory that could serve as an alternative to Cantor's set theory. The ideas of the alternative set theory make it possible to constitute a new approach to mathematics. An effort to formalize mathematically our intuitive concepts once more is made, and moreover it seems that one can obtain in the alternative set theory mathematical formalizations of concepts which up to now were not adequately formalized. In the alternative set theory we can build up all essential parts of mathematics. Development of the classical disciplines is described in [V]. Let us mention a few further results obtained in the alternative set theory: a connection between the discrete and the continuous on the basis of which it is possible to define topology (cf. [V]), investigation of motion (cf. [V]), construction of different types of σ-additive ultrafilters (cf. [S-V4]), classification of classes (measurement of vagueness of properties; cf. [Č-V]), possibility of definition of notions of nonstandard methods (cf. [S-V 1]) and valuations of ideals (cf. [M]). A series of articles has been written developing mathematics in the alternative set theory (for the full list of papers cf. [S]). For some remarks concerning the connection between the alternative set theory and nonstandard methods, the reader is refered to [S 4].