We identify two new clusters of proof complexity measures equal up to polynomial and log ⁡ n factors. The first cluster contains the logarithm of tree-like resolution size, regularized clause and monomial space, and clause space, ordinary and regularized, in regular and tree-like resolution. Consequently, separating clause or monomial space from the logarithm of tree-like resolution size is equivalent to showing strong trade-offs between clause space and length, and equivalent to showing super-critical trade-offs between clause space and depth. The second cluster contains width, Σ 2 space (a generalization of clause space to depth 2 Frege systems), ordinary and regularized, and the logarithm of tree-like R ( log ⁡ ) size. As an application, we improve a known size-space trade-off for polynomial calculus with resolution. We further show a quadratic lower bound on tree-like resolution size for formulas refutable in clause space 4, and introduce a measure intermediate between depth and the logarithm of tree-like resolution size.

We prove that for k ≪ 4√ n regular resolution requires length n Ω( k ) to establish that an Erdős–Rényi graph with appropriately chosen edge density does not contain a k -clique. This lower bound is optimal up to the multiplicative constant in the exponent and also implies unconditional n Ω( k ) lower bounds on running time for several state-of-the-art algorithms for finding maximum cliques in graphs.

We prove that CDCL SAT-solvers with the ordered decision strategy and the DECISION learning scheme are equivalent to ordered resolution. We also prove that, by replacing this learning scheme with its opposite, which learns the first possible non-conflict clause, they become equivalent to general resolution. In both results, we allow nondeterminism in the solver’s ability to perform unit propagation, conflict analysis, and restarts in a way that is similar to previous works in the literature. To aid the presentation of our results, and possibly future research, we define a model and language for CDCL-based proof systems – particularly those with nonstandard features – that allow for succinct and precise theorem statements.

We prove that for k ≪ n1/4 regular resolution requires length nΩ(k) to establish that an Erdos-Renyi graph with appropriately chosen edge density does not contain a k-clique. This lower bound is optimal up to the multiplicative constant in the exponent, and also implies unconditional nΩ(k) lower bounds on running time for several state-of-the-art algorithms for finding maximum cliques in graphs.

Let $P$ be a fixed graph (hereafter called a “pattern''), and let ${\sc Subgraph}(P)$ denote the problem of deciding whether a given graph $G$ contains a subgraph isomorphic to $P$. We are interested in $AC^0$-complexity of this problem, determined by the smallest possible exponent $C(P)$ for which ${\sc Subgraph}(P)$ possesses bounded-depth circuits of size $n^{C(P)+o(1)}$. Motivated by the previous research in the area, we also consider its “colorful” version ${\sc Subgraph}_\mathsf{col}(P)$ in which the target graph $G$ is $V(P)$-colored, and the average-case version ${\sc Subgraph}_\mathsf{ave}(P)$ under the distribution $G(n,n^{-\theta(P)})$, where $\theta(P)$ is the threshold exponent of $P$. Defining $C_\mathsf{col}(P)$ and $C_\mathsf{ave}(P)$ analogously to $C(P)$, our main contributions can be summarized as follows: (1) $C_\mathsf{col}(P)$ coincides with the treewidth of the pattern $P$ up to a logarithmic factor. This shows that the previously known upper bound by Alon, Yuster, and Zwick [ J. ACM, 42 (1995), pp. 844--856] is almost tight. (2) We give a characterization of $C_\mathsf{ave}(P)$ in purely combinatorial terms up to a multiplicative factor of 2. This shows that the lower bound technique of Rossman [ Proceedings of the 40th ACM Symposium on Theory of Computing, 2008, pp. 721--730] is essentially tight for any pattern $P$ whatsoever. (3) We prove that if $Q$ is a minor of $P$, then ${\sc Subgraph}_\mathsf{col}(Q)$ is reducible to ${\sc Subgraph}_\mathsf{col}(P)$ via a linear-size monotone projection. At the same time, we show that there is no monotone projection whatsoever that reduces ${\sc Subgraph}(M_3)$ to ${\sc Subgraph}(P_3 + M_2)$ ($P_3$ is a path on three vertices, $M_k$ is a matching with $k$ edges, and “+” stands for the disjoint union). This result strongly suggests that the colorful version of the subgraph isomorphism problem is much better structured and well-behaved than the standard (worst-case, uncolored) one.

We exhibit an unusually strong tradeoff in propositional proof complexity that significantly deviates from the established pattern of almost all results of this kind. Namely, restrictions on one resource (width, in our case) imply an increase in another resource (tree-like size) that is exponential not only with respect to the complexity of the original problem, but also to the whole class of all problems of the same bit size. More specifically, we show that for any parameter k = k ( n ), there are unsatisfiable k -CNFs that possess refutations of width O ( k ), but such that any tree-like refutation of width n 1 − ϵ / k must necessarily have doubly exponential size exp ( n Ω( k ) ). This means that there exist contradictions that allow narrow refutations, but in order to keep the size of such a refutation even within a single exponent, it must necessarily use a high degree of parallelism. Our construction and proof methods combine, in a non-trivial way, two previously known techniques: the hardness escalation method based on substitution formulas and expansion. This combination results in a hardness compression approach that strives to preserve hardness of a contradiction while significantly decreasing the number of its variables.

Let P be a fixed graph (hereafter called a “pattern”), and let SUBGRAPH(P) denote the problem of deciding whether a given graph G contains a subgraph isomorphic to P. We are interested in AC0-complexity of this problem, determined by the smallest possible exponent C(P) for which SUBGRAPH(P) possesses bounded-depth circuits of size nC(P)+o(1). Motivated by the previous research in the area, we also consider its “colorful” version SUBGRAPHcol(P) in which the target graph G is V(P)colored, and the average-case version SUBGRAPHave(P) under the distribution G(n, n-θ(P)), where θ(P) is the threshold exponent of P. Defining Ccol(P) and Cave(P) analogously to C(P), our main contributions can be summarized as follows. (1) Ccol(P) coincides with the tree-width of the pattern P within a logarithmic factor. This shows that the previously known upper bound by Alon, Yuster, Zwick [3] is almost tight. (2) We give a characterization of Cave(P) in purely combinatorial terms within a multiplicative factor of 2. This shows that the lower bound technique of Rossman [21] is essentially tight, for any pattern P whatsoever. (3) We prove that if Q is a minor of P then SUBGRAPHcol(Q) is reducible to SUBGRAPHcol(P) via a linear-size monotone projection. At the same time, we show that there is no monotone projection whatsoever that reduces SUBGRAPH(M3) to SUBGRAPH(P3+ M2) (P3is a path on 3 vertices, Mk is a matching with k edges, and “+” stands for the disjoint union). This result strongly suggests that the colorful version of the subgraph isomorphism problem is much better structured and well-behaved than the standard (worstcase, uncolored) one.

A general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider [9]. There the authors concentrate on tree-like Parameterized Resolution—a parameterized version of classical Resolution—and their gap complexity theorem implies lower bounds for that system. The main result of the present paper significantly improves upon this by showing optimal lower bounds for a parameterized version of bounded-depth Frege. More precisely, we prove that the pigeonhole principle requires proofs of size n Ω(k) in parameterized bounded-depth Frege, and, as a special case, in dag-like Parameterized Resolution. This answers an open question posed in [9]. In the opposite direction, we interpret a well-known technique for FPT algorithms as a DPLL procedure for Parameterized Resolution. Its generalization leads to a proof search algorithm for Parameterized Resolution that in particular shows that tree-like Parameterized Resolution allows short refutations of all parameterized contradictions given as bounded-width CNF’s.

The sign-rank of a matrix $A=[A_{ij}]$ with $\pm1$ entries is the least rank of a real matrix $B=[B_{ij}]$ with $A_{ij}B_{ij}>0$ for all $i,j$. We obtain the first exponential lower bound on the sign-rank of a function in $\mathsf{AC}^0$. Namely, let $f(x,y)=\bigwedge_{i=1,\dots,m}\bigvee_{j=1,\dots,m^2}(x_{ij}\wedge y_{ij})$. We show that the matrix $[f(x,y)]_{x,y}$ has sign-rank $\exp(\Omega(m))$. This in particular implies that $\Sigma_2^{cc}\not\subseteq\mathsf{UPP}^{cc}$, which solves a longstanding open problem in communication complexity posed by Babai, Frankl, and Simon [Proceedings of the 27th Symposium on Foundations of Computer Science (FOCS), 1986, pp. 337–347]. Our result additionally implies a lower bound in learning theory. Specifically, let $\phi_1,\dots,\phi_r:\{0,1\}^n\to\mathbb{R}$ be functions such that every DNF formula $f:\{0,1\}^n\to\{-1,+1\}$ of polynomial size has the representation $f\equiv\mathrm{sgn}(a_1\phi_1+\dots+a_r\phi_r)$ for some reals $a_1,\dots,a_r$. We prove that then $r\geqslant\exp(\Omega(n^{1/3}))$, which essentially matches an upper bound of $\exp(\tilde{O}(n^{1/3}))$, due to Klivans and Servedio [J. Comput. System Sci., 68 (2004), pp. 303–318]. Finally, our work yields the first exponential lower bound on the size of threshold-of-majority circuits computing a function in $\mathsf{AC}^0$. This substantially generalizes and strengthens the results of Krause and Pudlák [Theoret. Comput. Sci., 174 (1997), pp. 137–156].

Every 3-graph in which no four vertices are independent and no four vertices span precisely three edges must have edge density $\geq4/9(1-o(1))$. This bound is tight. The proof is a rather elaborate application of Cauchy–Schwarz-type arguments presented in the framework of flag algebras. We include further demonstrations of this method by re-proving a few known tight results about hypergraph Turán densities and significantly improving numerical bounds for several problems for which the exact value is not known yet.

The sign-rank of a matrix A = [Aij] with plusmn1 entries is the least rank of a real matrix B = [Bij] with AijBij> 0 for all i, j. We obtain the first exponential lower bound on the sign-rank of a function in AC0. Namely, let f(x, y) = Lambdai=1mLambdaj=1m2(xijLambda yij). We show that the matrix [f(x, y)]x,yhas sign-rank 2Omega(m). This in particular implies that Sigma2ccnsubeUPPcc, which solves a long-standing open problem posed by Babai, Frankl, and Simon (1986). Our result additionally implies a lower bound in learning theory. Specifically, let Phi1,..., Phir: {0, 1}nrarrRopf be functions such that every DNF formula f : {0, 1}nrarr {-1, +1} of polynomial size has the representation f equiv sign(a1Phi1+ hellip + arPhir) for some reals a1,..., ar. We prove that then r ges 2Omega(n1/3), which essentially matches an upper bound of 2Otilde(n1/3)due to Klivans and Servedio (2001). Finally, our work yields the first exponential lower bound on the size of threshold-of-majority circuits computing a function in AC0. This substantially generalizes and strengthens the results of Krause and Pudlak (1997).

We show that neither resolution nor tree-like resolution is automatizable unless the class W[P] from the hierarchy of parameterized problems is fixed-parameter tractable by randomized algorithms with one-sided error.

Abstract Asymptotic extremal combinatorics deals with questions that in the language of model theory can be re-stated as follows. For finite models M, N of an universal theory without constants and function symbols (like graphs, digraphs or hypergraphs), let p(M, N) be the probability that a randomly chosen sub-model of N with ∣M∣ elements is isomorphic to M. Which asymptotic relations exist between the quantities p(M1,N),…, p(Mh,N), where M1,…, M1, are fixed “template” models and ∣N∣ grows to infinity? In this paper we develop a formal calculus that captures many standard arguments in the area, both previously known and apparently new. We give the first application of this formalism by presenting a new simple proof of a result by Fisher about the minimal possible density of triangles in a graph with given edge density.

A two server private information retrieval (PIR) scheme allows a user U to retrieve the i-th bit of an n-bit string x replicated between two servers while each server individually learns no information about i. The main parameter of interest in a PIR scheme is its communication complexity, namely the number of bits exchanged by the user and the servers. A large amount of effort has been invested by researchers over the last decade in search for efficient PIR schemes. A number of different schemes ((B. Chor. O. Goldreich. E. Kushilevitz. and M. Sudan, 1998), (A. Beimel and Y. Ishai, 2001) ,(D. Woodruff and S. Yekhanin, 2005)) have been proposed, however all of them ended up with the same communication complexity of O(n1/3). The best known lower bound to date is 5 log n by (S. Wehner and R. de Wolf, 2005) . The tremendous gap between upper and lower bounds is the focus of our paper. We show an Omega(n1/3) lower bound in a restricted model that nevertheless captures all known upper bound techniques. Our lower bound applies to bilinear group based PIR schemes. A bilinear PIR scheme is a one round PIR scheme, where user computes the dot product of servers' responses to obtain the desired value of the i-th bit. Every linear scheme can be turned into a bilinear one with an asymptotically negligible communication overhead. A group based PIR scheme is a PIR scheme that involves servers representing database by a function on a certain finite group G, and allows user to retrieve the value of this function at any group element using the natural secret sharing scheme based on G. Our proof relies on representation theory of finite groups

A theorem by Lin and Zhao shows how to turn any nondisjunctive logic program, understood in accordance with the answer set semantics, into an equivalent set of propositional formulas. The set of formulas generated by this process can be significantly larger than the original program. In this article we show (assuming P ⊈ NC 1 / poly , a conjecture from the theory of computational complexity that is widely believed to be true) that this is inevitable: any equivalent translation from logic programs to propositional formulas involves a significant increase in size.

A computation or a proof is called feasible if it obeys prescribed bounds on the resources consumed during its execution. It turns out that when restricted to this world of feasibility, proofs and computations become extremely tightly interrelated, sometimes even indistinguishable. Moreover, many of these rich relations, underlying concepts, techniques etc. look very different from their "'classical" counterparts, or simply do not have any. This paper is intended as a very informal and popular (highly biased as well) attempt to illustrate these fascinating connections by several related developments in the modern complexity theory.

We call a pseudorandom generator $G_n:\{0,1\}^n\to \{0,1\}^m$ hard for a propositional proof system P if P cannot efficiently prove the (properly encoded) statement $G_n(x_1,\ldots,x_n)\neq b$ for any string $b\in\{0,1\}^m$. We consider a variety of "combinatorial" pseudorandom generators inspired by the Nisan--Wigderson generator on the one hand, and by the construction of Tseitin tautologies on the other. We prove that under certain circumstances these generators are hard for such proof systems as resolution, polynomial calculus, and polynomial calculus with resolution (PCR).

article Share on Propositional proof complexity Author: Alexander Razborov Institute for Advanced Study, Princeton, New Jersey, and Steklov Mathematical Institute, Moscow, Russia Institute for Advanced Study, Princeton, New Jersey, and Steklov Mathematical Institute, Moscow, RussiaView Profile Authors Info & Claims Journal of the ACMVolume 50Issue 1pp 80–82https://doi.org/10.1145/602382.602406Published:01 January 2003Publication History 2citation1,113DownloadsMetricsTotal Citations2Total Downloads1,113Last 12 Months7Last 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 SiteGet Access

For an arbitrary hypergraph H let PM(H) be the propositional formula asserting that H contains a perfect matching. We show that every resolution refutation of PM(H) must have size exp((/spl Omega/(/spl delta/(H)//spl lambda/(H)r(H)(log n(H))(r(H)+log n(H)))), where n(H) is the number of vertices, /spl delta/(H) is the minimal degree of a vertex, r(H) is the maximal size of an edge, and /spl lambda/(H) is the maximal number of edges incident to two different vertices. For ordinary graphs G our general bound considerably simplifies to exp (/spl Omega/(/spl delta/(G)/(log n(G))/sup 2/))). As a direct corollary, every resolution proof of the functional onto a version of the pigeonhole principle onto - FPHP/sub n//sup m/ must have size exp (/spl Omega/(n/(log m)/sup 2/)) (which becomes exp (/spl Omega/(n/sup 1/3/)) when the number of pigeons m is unbounded). This in turn immediately implies an exp(/spl Omega/(t/n/sup 3/)) lower bound on the size of resolution proofs of the principle circuit/sub t/(f/sub n/) asserting that the circuit size of the Boolean function f/sub n/ in n variables is greater than t. In particular resolution does not possess efficient proofs of NP /spl subne/ P/poly. These results relativize, in a natural way, to more general principle M(U|H) asserting that H contains a matching covering all vertices in U /spl sube/ V(H).

For a CNF /spl tau/, let w/sub b/(/spl tau/) be the branch-width of its underlying hypergraph. In this paper we design an algorithm for solving SAT in time n/sup O(1)/2/sup O(w(b)(/spl tau/))/. This in particular implies a polynomial algorithm for testing satisfiability on instances with tree-width O(log n). Our algorithm is a modification of the width based automated theorem prover (WBATP) which is a popular (at least on the theoretical level) heuristic for finding resolution refutations of unsatisfiable CNFs. We show that instead of the exhaustive enumeration of all provable clauses, one can do a better search based on the Robertson-Seymour algorithm for approximating the branch-width of a graph. We call the resulting procedure Branch-Width Based Automated Theorem Prover (BWBATP). As opposed to WBATP, it always produces regular refutations. Perhaps more importantly, the running time of our algorithm is bounded in terms of a clean combinatorial characteristic that can be efficiently approximated, and that the algorithm also produces, within the same time, a satisfying assignment if /spl tau/ happens to be satisfiable. In the second part of the paper we investigate the behavior of BWBATP on the Well-studied class of Tseitin tautologies. We argue that in this case BWBATP is better than WBATP. Namely, we show that its running time on any Tseitin tautology /spl tau/ is |/spl tau/|/sup O(1)/. 2/sup O(w(/spl tau//spl boxvr/O))/ as opposed to the obvious bound n/sup O(w(/spl tau//spl boxvr/O))/ provided by WBATP. This in particular implies that Resolution is automatizable on those Tseitin tautologies for which we know the relation w(/spl tau//spl boxvr//spl phi/) /spl les/ O(log S(/spl tau/)). We identify one such subclass and prove partial results toward establishing this relation for larger classes of graphs.

We study space complexity in the framework of propositional proofs. We consider a natural model analogous to Turing machines with a read-only input tape and such popular propositional proof systems as resolution, polynomial calculus, and Frege systems. We propose two different space measures, corresponding to the maximal number of bits, and clauses/monomials that need to be kept in the memory simultaneously. We prove a number of lower and upper bounds in these models, as well as some structural results concerning the clause space for resolution and Frege systems.

We generalize recent linear lower bounds for Polynomial Calculus based on binomial ideals. We produce a general hardness criterion (that we call immunity) which is satisfied by a random function and prove linear lower bounds on the degree of PC refutations for a wide class of tautologies based on immune functions. As some applications of our techniques, we introduce mod/sub p/ Tseitin tautologies in the Boolean case (e.g. in the presence of axioms x/sub i//sup 2/=x/sub i/), prove that they are hard for PC over fields with characteristic different from p, and generalize them to Flow tautologies which are based on the MAJORITY function and are proved to be hard over any field. We also show the /spl Omega/(n) lower bound for random k-CNFs over fields of characteristic 2.

We show that neither Resolution nor tree-like Resolution is automatizable unless the class W[P] from the hierarchy of parameterized problems is fixed-parameter tractable by randomized algorithms with one-sided error.

We call a pseudorandom generator G/sub n/:{0,1}/sup n//spl rarr/{0,1}/sup m/ hard for a propositional proof system P if P can not efficiently prove the (properly encoded) statement G/sub n/(x/sub 1/,...,x/sub n/)/spl ne/b for any string b/spl epsiv/{0,1}/sup m/. We consider a variety of "combinatorial" pseudorandom generators inspired by the Nisan-Wigderson generator on one hand, and by the construction of Tseitin tautologies on the other. We prove that under certain circumstances these generators are hard for such proof systems as resolution, polynomial calculus and polynomial calculus with resolution (PCR).

A depth 3 arithmetic circuit can be viewed as a sum of products of linear functions. We prove an exponential complexity lower bound on depth 3 arithmetic circuits computing some natural symmetric functions over a finite field F. Also, we study the complexity of the functions f: D/sup n//spl rarr/F for subsets D/spl sub/F. In particular, we prove an exponential lower bound on the complexity of a depth 3 arithmetic circuit which computes the determinant or the permanent of a matrix considered as functions f:(F*)n/sup 2//spl rarr/F.

We investigate read-once branching programs for the following search problem: given a Boolean m n matrix with m>n, nd either an all-zero row, or two 1's in some column. Our primary motivation is that this models regular resolution proofs of the pigeonhole principle PHP m n, and that for m>n 2 no lower bounds are known for the length of such proofs. We prove exponential lower bounds (for arbitrarily large m!) if we further restrict this model by requiring the branching program either

Article Natural proofs Share on Authors: Alexander A. Razborov School of Mathematics, Institute for Advanced Study Princeton, NJ and Steklov Mathematical Institute Vavilova 42, 117966, GSP-1 Moscow, Russia School of Mathematics, Institute for Advanced Study Princeton, NJ and Steklov Mathematical Institute Vavilova 42, 117966, GSP-1 Moscow, RussiaView Profile , Steven Rudich Computer Science Department, Carnegie Mellon University, Pittsburgh, PA Computer Science Department, Carnegie Mellon University, Pittsburgh, PAView Profile Authors Info & Claims STOC '94: Proceedings of the twenty-sixth annual ACM symposium on Theory of ComputingMay 1994 Pages 204–213https://doi.org/10.1145/195058.195134Online:23 May 1994Publication History 49citation861DownloadsMetricsTotal Citations49Total Downloads861Last 12 Months21Last 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 SiteGet Access

Article Free Access Share on On the method of approximations Author: A. A. Razborov Steldov Mathematical Institute, 117966, MOSCOW, GSP-1, Vavilova, 42, USSR Steldov Mathematical Institute, 117966, MOSCOW, GSP-1, Vavilova, 42, USSRView Profile Authors Info & Claims STOC '89: Proceedings of the twenty-first annual ACM symposium on Theory of computingFebruary 1989 Pages 167–176https://doi.org/10.1145/73007.73023Published:01 February 1989Publication History 43citation447DownloadsMetricsTotal Citations43Total Downloads447Last 12 Months40Last 6 weeks5 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