Clique is hard on average for regular resolution

Clique Is Hard on Average for Regular Resolution Albert Atserias Universitat Politècnica de Catalunya Department of Computer Science Barcelona, Spain [email protected] Ilario Bonacina Universitat Politècnica de Catalunya Department of Computer Science Barcelona, Spain [email protected]c.edu Susanna F. de Rezende KTH Royal Institute of Technology School of Electrical Engineering and Computer Science Stockholm, Sweden [email protected] Massimo Lauria Sapienza Università di Roma Department of Statistical Sciences Rome, Italy [email protected] Jakob Nordström KTH Royal Institute of Technology School of Electrical Engineering and Computer Science Stockholm, Sweden [email protected] Alexander Razborov University of Chicago Chicago, USA [email protected] Steklov Mathematical Institute Moscow, Russia [email protected] ABSTRACT 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. CCS CONCEPTS •Theory of computation →Proof complexity ; •Mathematics of computing →Random graphs; KEYWORDS Proof complexity, regular resolution, k -clique, Erdős-Rényi random graphs ACM Reference Format: Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Alexander Razborov. 2018. Clique Is Hard on Average for Regular Resolution . In Proceedings of 50th Annual ACM SIGACT Symposium on the Theory of Computing (STOC’18). ACM, New York, NY, USA, 12 pages. https://doi.org/10.1145/3188745.3188856 1 INTRODUCTION Deciding whether a graph has a k -clique is one of the most basic computational problems on graphs, and has been extensively studied in computational complexity theory ever since it appeared in Karp’s list of 21 NP-complete problems [ 15 ]. Not only is this problem widely believed to be infeasible to solve exactly—unless P=NP there does not even exist any polynomial-time algorithm for approximating the maximal size of a clique to within a factor n1−ϵ for any constant ϵ> 0, where n is the number of vertices in the graph [ 13 , 34 ]. Furthermore, the problem appears to be hard not only in the worst case but also on average in the Erdős-Rényi random graph model—we know of no efficient algorithms for finding cliques of maximum size asymptotically almost surely on random graphs with appropriate edge densities [16,31]. In terms of upper bounds, the k -clique problem can clearly be solved in time roughly nk simply by checking if any of the n k many sets of vertices of size k forms a clique, which is polynomial if k is constant. This can be improved slightly to O (nωk/3) using algebraic techniques [ 26 ], where ω≤ 2 . 373 is the matrix multiplication exponent, although in practice such algebraic algorithms are outperformed by combinatorial ones [33]. The motivating problem behind this work is to determine the exact time complexity of the clique problem when k is given as a parameter. As noted above, all known algorithms require time nΩ(k) . It appears quite likely that some dependence on k is needed in the exponent, since otherwise we have the parameterized complexity collapse FPT =W [1] [ 11 ]. Even more can be said if we are willing to believe the Exponential Time Hypothesis (ETH) [ 14 ]—then the exponent has to depend linearly on k [ 8 ], so that the trivial upper bound is essentially tight. Obtaining such a lower bound unconditionally would, in particular, imply P,NP , and so currently seems completely out of reach. But is it possible to prove nΩ(k) lower bounds in restricted but nontrivial models of computation? For circuit complexity, this challenge has been met for circuits that are of bounded depth [ 30 ] or are monotone [ 32 ]. In this paper we focus on computational models that are powerful enough to capture algorithms that are used in practice. When analysing such algorithms, it is convenient to view the execution trace as a proof establishing the maximal clique size for the input graph. In particular, if this graph does not have a k -clique, then the trace provides an efficiently verifiable proof of the statement that the graph is k-clique -free. If one can establish a lower bound on the length of such proofs, then this implies a lower Definitive Version in the ACM Digital Library: https://dl.acm.org/citation.cfm? doid=3188745.3188856 bound on the running time of the algorithm, and this lower bound holds even if the algorithm is a non-deterministic heuristic that somehow magically gets to make all the right choices. This brings us to the topic of proof complexity [ 9 ], which can be viewed as the study of upper and lower bounds in restricted nondeterministic computational models. Using a standard reduction from k-clique to SAT, we can translate the problem of k-cliques in graphs to that of satisfiability of formulas in conjunctive normal form (CNF). If an algorithm for finding k -cliques is run on a graph G that is k-clique -free, then we can extract a proof of the unsatisfiability of the corresponding CNF formula—the k -clique formula on G —from the execution trace of the algorithm. Is it possible to show any non-trivial lower bound on the length of such proofs? Specifically, does the resolution proof system—the method of reasoning underlying state-of-the-art SAT solvers [ 2 , 23 , 25 ]—require length nΩ(k) , or at least nωk(1) , to prove the absence of k -cliques in a graph? This question was asked in, e.g., [7] and remains open. The hardness of k -clique formulas for resolution is also a problem of intrinsic interest in proof complexity, since these formulas escape known methods of proving resolution lower bounds for a range of interesting values of k including k= O ( 1 ) . In particular, the interpolation technique [ 18 , 28 ], the random restriction method [ 4 ], and the size-width lower bound [5] all seem to fail. To make this more precise, we should mention that some previous works do use the size-width method, but only for very large k . It was shown in [ 3 ] that for n5/6≪k≤n/ 3resolution requires length expnΩ(1) to certify that a dense enough Erdős-Rényi random graph is k -clique-free. The constant hidden in the Ω( 1 ) increases with the density of the graph and, in particular, for very dense graphs and k=n/ 3the length required is 2 Ω(n) . Also, for a specially tailored CNF encoding, where the i th member of the claimed k -clique is encoded in binary by logn variables, a lower bound of nΩ(k) for k≤logn can be extracted from a careful reading of [ 21 ]. However, in the more natural unary encodings, where indicator variables specify whether a vertex is in the clique, the size-width method cannot yield more than a 2 Ω(k2/n) lower bound since there are resolution proofs of width O (k) . This bound becomes trivial when k≤√n. In the restricted subsystem of tree-like resolution, optimal nΩ(k) length lower bounds were established in [ 6 ] for k -clique formulas on complete (k−1)-partite as well as on average for Erdős-Rényi random graphs of appropriate edge density. There is no hope to get hard instances for general resolution from complete (k−1)-partite graphs, however—in the same paper it was shown that all instances from the more general class of (k− 1 ) -colourable graphs are easy for resolution. A closer study of these resolution proofs reveals that they are regular, meaning that if the proof is viewed as a directed acyclic graph (DAG), then no variable is eliminated more than once on any source-to-sink path. More generally, regular resolution is an interesting and nontrivial model to analyse for the k -clique problem since it captures the reasoning used in many state-of-the-art algorithms used in practice (for a survey, see, e.g., [ 24 , 27 ]). Nonetheless, it has remained consistent with state-of-the-art knowledge that for k≤n5/6 regular resolution might be able to certify k-clique -freeness in polynomial length independent of the value of k. Our contribution. We prove optimal nΩ(k) average-case lower bounds for regular resolution proofs of unsatisfiability for k -clique formulas on Erdős-Rényi random graphs. Theorem 1.1 (Informal). For any integer k≪4 √n , given an n -vertex graph G sampled at random from the Erdős-Rényi model with the appropriate edge density, regular resolution asymptotically almost surely requires length nΩ(k) to certify that G does not contain ak-clique. In order to make this formal, we need to define how the problem is encoded: depending on the formula considered, the exact statement of what we can prove differs. In this conference paper we consider the simpler encoding for which we can prove an nΩ(k) lower bound for k≪√n . For a stronger encoding, which in particular captures this simpler one, we prove the above result in the full-length version of this paper. At a high level, the proof is based on a bottleneck counting argument in the style of [ 12 ] with a slight twist that was introduced in [ 29 ]. In its classical form, such a proof takes four steps. First, one defines a distribution of random source-to-sink paths on the DAG representation of the proof. Second, a subset of the vertices of the DAG is identified—the set of bottleneck nodes—such that any random path must necessarily pass through at least one such node. Third, for any fixed bottleneck node, one shows that it is very unlikely that a random path passes through this particular node. Given this, a final union bound argument yields the conclusion that the DAG must have many bottleneck nodes, and so the resolution proof must be long. The twist in our argument is that, instead of single bottleneck nodes, we need to define bottleneck pairs of nodes. We then argue that any random path passes through at least one such pair but that few random paths pass through any fixed pair; the latter part is based on Markov chain-type reasoning similar to [ 29 , Theorems 3.2, 3.5]. Furthermore, it crucially relies on that the graph satisfies a certain combinatorial property, which captures the idea that the common neighbourhood of a small set of vertices is well distributed across the graph. Identifying this combinatorial property is a key contribution of our work. In a separate argument (that, surprisingly, turned out to be much more elaborate than most arguments of this kind) we then establish that Erdős-Rényi random graphs of the appropriate edge density satisfy this property asymptotically almost surely. Combining these two facts yields our average-case lower bound. Another contribution of this paper is a relatively simple observation that not only is regular resolution powerful enough to distinguish graphs that contain k -cliques from (k− 1 ) -colourable graphs [ 6 ], but it can also distinguish them from graphs that have a homomorphism to any fixed graph Hwith no k-cliques. Paper outline. The rest of this paper is organized as follows. Section 2presents some preliminaries. We show that some nontrivial k -clique instances are easy for regular resolution in Section 3. Section 4contains the formal statement of the lower bounds we prove for Erdős-Rényi random graphs. In Section 5we define a combinatorial property of graphs and show that clique formulas on such graphs are hard for regular resolution, and the proof that Erdős- Rényi random graphs satisfy this property asymptotically almost surely is in Section 6. We conclude in Section 7with a discussion of open problems. 2 PRELIMINARIES We write G=(V,E) to denote a graph with vertices V and edges E , where G is always undirected, without loops and multiple edges. Given a vertex v∈V , we write N(v)={u|there exists v∈V such that {u,v} ∈ E} to denote the set of neighbours of v . For a set of vertices R⊆V we write b N(R)=Ñv∈RN(v) to denote the set of common neighbours of R . For two sets of vertices R⊆V and W⊆V we write b NW(R)=b N(R) ∩W to denote the set of common neighbours of R inside W . For a set U⊆V we denote by G[U] the subgraph of G induced by the set U . For n∈N+ we write [n]={ 1 , . . . , n} . We say that V1 . ∪V2 . ∪ ··· . ∪Vk=V is a balanced k -partition of V if for all i,j∈ [k] it holds that |Vi|≤|Vj|+ 1. All logarithms are natural (base e) if not specified otherwise. Probability and Erdős-Rényi random graphs. We denote random variables in boldface and write X∼D to denote that X is sampled from the distribution D. A p-biased coin, or a Bernoulli variable, is the outcome of a coin flip that yields 1with probability p and 0with probability 1 −p . We use the special case of Markov’s inequality saying that if X is non-negative, then Pr[X≥ 1 ] ≤ E[X] . We also need the following special case of the multiplicative Chernoff bound: if X is a binomial random variable (i.e., the sum of i.i.d. Bernoulli variables) with expectation µ=E[X], then Pr[X≤µ/2] ≤ e−µ/8. We consider the Erdős-Rényi distribution G(n,p) of random graphs on a fixed set V of n vertices. A random graph sampled from G(n,p) is produced by placing each potential edge {u,v} independently with probability p ,0 ≤p≤ 1(the edge probability p may be a function of n ). A property of graphs is said to hold asymptotically almost surely on G(n,p(n)) if it holds with probability that approaches 1as napproaches infinity. For a positive integer k , let Xk be the random variable that counts the number of k -cliques in a random graph from G(n,p) . It follows from Markov’s inequality that asymptotically almost surely there are no k -cliques in G(n,p) whenever p and k are such that E[Xk]=p(k 2)n k approaches 0as n approaches infinity. This is the case, for example, if p=n−2η/(k−1)for k≥2and η>1. CNF formulas and resolution. Aliteral over a Boolean variable x is either the variable x itself (a positive literal) or its negation ¬x (a negative literal). A clause C=a1∨···∨aw is a disjunction of literals; we say that the width of C is w . The empty clause will be denoted by ⊥ . A CNF formula F=C1∧···∧Cm is a conjunction of clauses. We think of clauses as sets of literals and of CNF formulas as sets of clauses, so that order is irrelevant and there are no repetitions. For a formula Fwe denote by Vars(F)the set of variables of F. Aresolution derivation from a CNF formula F is as an ordered sequence of clauses π=(D1, . . . , DL) such that for each i∈ [L] either Di is a clause in F or there exist j<i and k<i such that Di is derived from Djand Dkby the resolution rule B∨x C ∨¬x B∨C,(1) Di=B∨C,Dj=B∨x,Dk=C∨¬x . We refer to B∨C as the resolvent of B∨x and C∨¬x over x , and to x as the resolved variable. The length (or size) of a resolution derivation π=(D1, . . . , DL) is L and it is denoted by |π| . A resolution refutation of F , or resolution proof for (the unsatisfiability of) F , is a resolution derivation from F that ends in the empty clause ⊥. A resolution derivation π=(D1, . . . , DL) can also be viewed as a labelled DAG with set of nodes { 1 , . . . , L} and edges (j,i) , (k,i) for each application of the resolution rule deriving Di from Dj and Dk . Each node i in this DAG is labelled by its associated clause Di , and each non-source node is also labelled by the resolved variable in its associated derivation step in the refutation. A resolution refutation is called regular if along any source-to-sink path in its associated DAG every variable is resolved at most once. For a partial assignment ρ we say that a clause C restricted by ρ , denoted C↾ρ , is the trivial 1-clause if any of the literals in C is satisfied by ρ or otherwise is C with all falsified literals removed. We extend this definition to CNFs in the obvious way: (C1∧. . . ∧Cm)↾ρ=C1↾ρ∧. . . ∧Cm↾ρ . Applying a restriction preserves (regular) resolution derivations. To see this, observe that in every application of the resolution rule the restricted consequence is either killed (becomes identically 1) or obtained, as before, by resolving the two restricted premises or it is a copy of one of them. Thus, we have: Fact 2.1. Let π be a (regular) resolution refutation of a CNF formula F . For any partial assignment ρ to the variables of F there is an efficiently constructible (regular) resolution refutation π↾ρ of the CNF formula F↾ρ , so that the length of π↾ρ is at most the length of π . Branching programs. A branching program on variables x1, . . . , xn is a DAG that has one source node and where every non-sink node is labelled by one of the variables x1, . . . , xn and has exactly two outgoing edges labelled 0and 1. The size of a branching program is the total number of nodes in the graph. In a read-once branching program it holds in addition that along every path every variable appears as a node label at most once. For each node a in a branching program, let X(a) denote the variable that labels a , and let a0 and a1 be the nodes that are reached from a through the edges labelled 0and 1, respectively. A truthvalue assignment σ : {x1, . . . , xn} → { 0 , 1 } determines a path in a branching program in the following way. The path starts at the source node. At an internal node a , the path is extended along the edge labelled σ(X(a)) so that the next node in the path is aσ(X(a)) . The path ends when it reaches a sink. We write path(σ) for the path determined by σ . When extending the path from a node a to the node aσ(X(a)) , we say that the answer to the query X(a) at a is σ(X(a)) and that the path sets the variable X(a) to the value σ(X(a)) . For each node a of the branching program, let β(a) be the maximal partial assignment that is contained in any assignment σ such that path(σ) passes through a . Equivalently, this is the set of all those σ(xi)=γ for which the query xi is made, and answered by γ , along every consistent path from the source to a . If the program is read-once, the consistency condition becomes redundant. The falsified clause search problem for an unsatisfiable CNF formula F is the task of finding a clause C∈F that is falsified by a given truth value assignment σ . A branching program P on the variables Vars(F) solves the falsified clause search problem for F if each sink is labelled by a clause of F such that for every assignment σ , the clause that labels the sink reached by path(σ) is falsified by σ . The minimal size of any regular resolution refutation of an unsatisfiable CNF formula F is exactly the same as the minimal size of any read-once branching program solving the falsified clause search problem for F . This can be seen by taking the refutation DAG and reversing the edges to get a branching program or vice versa. For a formal proof see, e.g., [19, Theorem 4.3]. The k -clique formula. In order to analyse the complexity of resolution proofs that establish that a given graph does not contain a k -clique we must formulate the problem as a propositional formula in conjunctive normal form (CNF). We consider two distinct encodings for the clique problem originally defined in [3]. The first propositional encoding we present, Clique(G,k) , is based on mapping of vertices to clique members. This formula is defined over variables xv,i(v∈V,i∈ [k]) and consists of the following set of clauses: ¬xu,i∨¬xv,ji,j∈ [k],i,j,u,v∈V,{u,v}<E,(2a) Ü v∈V xv,ii∈ [k],(2b) ¬xu,i∨¬xv,ii∈ [k],u,v∈V,u,v,(2c) We refer to (2a) as edge axioms, (2b) as clique axioms and (2c) as functionality axioms. Note that Clique(G,k) is satisfiable if and only if G contains a k -clique, and that this is true even if clauses (2c) are omitted—we write Clique∗(G,k) to denote this formula with only clauses (2a) and (2b). The second version of clique formulas that we consider is the block encoding Cliqueblock(G,k) . This formula differs from the previous ones in that it requires a k -clique that has a certain “blockrespecting” structure. Let V1Û ∪V2Û ∪. . . Û ∪Vk=V be a balanced k - partition of V . This formula, defined over variables xv , encodes the fact that the graph contains a transversal k -clique, that is, a k -clique in which each clique member belongs to a different block. Formally, for any positive k and n , the formula Cliqueblock(G,k) consists of the following set of clauses: ¬xu∨¬xvu,v∈V,u,v,{u,v}<E,(3a) Ü v∈Vi xvi∈ [k],(3b) ¬xu∨¬xvi∈ [k],u,v∈Vi,u,v.(3c) Note that a graph can contain a k -clique but contain no transversal k -clique for a given partition. Intuitively it is clear that proving that a graph does not contain a transversal k -clique should be easier than proving it does not contain any k -clique, since any proof of the latter fact must in particular establish the former. We make this intuition formal below. Lemma 2.2 ([ 3 ]). For any graph G and any k∈N+ , the size of a minimum regular resolution refutation of Clique(G,k)is bounded from below by the size of a minimum regular resolution refutation of Cliqueblock(G,k). This lemma was proven in [ 3 ] for tree-like and for general resolution via a restriction argument, and it is straightforward to see that the same proof holds for regular resolution. 3 EASY GRAPHS FOR REGULAR RESOLUTION Before proving our main nΩ(k) lower bound, in this section we exhibit classes of graphs whose clique formulas have regular resolution refutations of fixed-parameter tractable length, i.e., length f(k) · nO(1) for some function f . This illustrates the strength of regular resolution for the k -clique problem. We note that the upper bounds claimed in this section hold not only for Clique(G,k) but even for the subformula Clique∗(G,k) that omits the functionality axioms (2c). The first example is the class of (k− 1 ) -colourable graphs. Such graphs are hard for tree-like resolution [ 6 ], and the known algorithms that distinguish them from graphs that contain k -cliques are highly non-trivial [ 17 , 22 ]. The second example is the class of graphs that have a homomorphism into a fixed k -clique free graph. Recall that a homomorphism from a graph G=(V,E) into a graph G′=(V′,E′) is a mapping h : V→V′ that maps edges {u,v} ∈ E into edges {h(u),h(v)} ∈ E′ . A graph is (k− 1 ) -colourable if and only if it has a homomorphism into the (k− 1 ) -clique, which is of course k -clique free. Therefore our second example is a generalization of the first one (but the function f(k)becomes larger). Both upper bounds follows from a generic procedure, based on Algorithm 1, that builds read-once branching programs for the falsified clause search problem for Clique∗(G,k). Given a k-clique free graph Gdefine I(G)=Gb N(R):Ris a clique in G.(4) Proposition 3.1. There is an efficiently constructible read-once branching program for the falsified clause search problem on formula Clique∗(G,k)of size at most |I(G)| ·k2· |V(G)|2. Proof. We build the branching program recursively, following the strategy laid out by Algorithm 1. For the base case k= 1, G must be the graph with no vertices. The branching program is a single sink node that outputs the clique axiom of index 1, i.e., the empty clause. For k> 1, fix n=|V(G)| and an ordering v1, . . . ,vn of the vertices in V(G) . We first build a decision tree T by querying the variables xv1,k,xv2,k, . . . in order, until we get an answer 1, or until all variables with second index k have been queried. If xvj,k= 0 for all j∈ [n] then the k th clique axiom (2b) is falsified by the assignment (see line 14). Otherwise, let v be the first vertex in the order where xv,k= 1. The decision tree now queries xw,i for all w<N(v) and all i<k to check whether an edge axiom involving v is falsified (lines 4–6). If any of these variables is set to 1the branching stops and the leaf node is labelled with the corresponding edge axiom ¬xv,k∨¬xw,i. The decision tree T built so far has at most kn2 nodes, and we can identify n “open” leaf nodes av1,av2, . . . , avn , where avi is the leaf node reached by the path that sets xvi,k= 1and that does yet determine the answer to the search problem. Let us focus on a specific node av for some v∈V(G) . The partial assignment path(av) sets v to be the k th member of the clique and no vertex in V(G)\N(v) to be in the clique. Let Gv be the subgraph induced Algorithm 1 Read-once branching program for the falsified clause search problem on Clique∗(G,k). Input k∈N+, a k-clique free graph G, an assignment α:{xv,ifor v∈V(G),i∈ [k]} → {0,1} Output A clause of Clique∗(G,k)falsified by α 1: procedure Search(G,k,α) 2: for v∈V(G)do 3: if α(xv,k)=1then 4: for w<N(v)and i<kdo 5: if α(xw,i)=1then 6: return edge axiom ¬xv,k∨¬xw,i(2a). 7: end if 8: end for 9: G′←G[N(v)] 10: α′←α restricted to variables xw,j for w∈V(G′) and 1≤j≤k−1 11: return Search(G′,k−1,α′) 12: end if 13: end for 14: return the kth clique axiom (2b). 15: end procedure on G by N(v) , let Sv be the set of variables xw,i for w∈N(v) and i<k , and let ρv be the partial assignment setting xw,i= 0for w<N(v)and i<k. Clearly ρv⊆path(av). By the inductive hypothesis there exists a branching program Bv that solves the search problem on Clique∗(Gv,k− 1 ) querying only variables in Sv . This corresponds to the recursive call for the subgraph Gv and k− 1(lines 9–11). If we attach each Bv to av we get a complete branching program for Clique∗(G,k) . This is readonce because Bv only queries variables in Sv and these variables are not in path(av). To prove that the composed program is correct we consider an assignment σ to the variables in Sv and show that the clause output by Bv on σ is also a valid output for the search problem on Clique∗(G,k) , i.e., it is falsified by the assignment path(av)∪σ . Actually we show the stronger claim that it is falsified by ρv∪σ , which is a subset of path(av)∪σ . To this end, note that if the output of Bv on σ is an edge axiom of Clique∗(Gv,k− 1 ) , this must be some ¬xu,i∨ ¬xw,j for i,j<k , which is also an edge axiom of Clique∗(G,k) and is falsified by σ⊆ρv∪σ . Now if the output of Bv on σ is the i th clique axiom of Clique∗(Gv,k− 1 ) , then σ falsifies Ôw∈N(v)xv,i , and therefore ρv∪σ falsifies the i th clique axiom in formula Clique∗(G,k). The construction so far is correct but produces a very large branching program (in particular, a tree-like one). In order to create a smaller branching program, we observe that if u,v∈V(G) are such that N(u)=N(w) then Gu=Gw , Bu=Bw and ρu=ρw . In this case, we can identify nodes au and aw , resulting in a node we denote a∗ , and identify the branching programs Bu and Bw . The correctness of this new program is due to the fact that even after the identification of vertices ρu⊆path(a∗) and ρw⊆path(a∗) . This process leads to having only one subprogram for each distinct induced subgraph at each level of the recursion. In order to bound the size of this program, we decompose it into k levels. The source is at level zero and corresponds to the graph G . At level i there are nodes corresponding to all subgraphs induced by the common neighbourhood of cliques of size i . Each node in the i th level connects to the nodes of the (i+ 1 ) th level by a branching program of size at most kn2 . Notice that an induced subgraph in I(G) cannot occur twice in the same layers, so the total size of the final branching program is at most |I(G)| ·k2n2 nodes. □ We now proceed to prove the upper bounds mentioned previously. A graph G that has a homomorphism into a small k -clique free graph H may still have a large set I(G) , making Proposition 3.1 inefficient. The first key observation is that if G has a homomorphism into a graph H then it is a subgraph of a blown up version of H , namely, of a graph obtained by transforming each vertex of H into a “cloud” of vertices where a cloud does not contain any edge, two clouds corresponding to two adjacent vertices in H have all possible edges between them, and two clouds corresponding to two non-adjacent vertices in H have no edges between them. A second crucial point is that if G′ is a blown up version of H then it turns out that |I(G′)| =|I(H)| , making Proposition 3.1 effective for G′ . The upper bound then follows from observing that the task of proving that G is k -clique free should not be harder than the same task for a supergraph of G . Indeed Fact 3.2 formalises this intuition. It is interesting to observe that the constructions in Proposition 3.1 and in Fact 3.2 are efficient. The non-constructive part is guessing the homomorphism to H. Fact 3.2. Let G=(V,E) and G′=(V′,E′) be graphs with no k -clique such that V⊆V′ and E⊆E′∩V 2 . If Clique∗(G′,k) has a (regular) refutation of length L , then Clique∗(G,k) also has a (regular) refutation of length L. Proof. Consider the partial assignment ρ that sets xv,i= 0for every v<V and i∈ [k] . The restricted formula Clique∗(G′,k)↾ρ is isomorphic to Clique∗(e G,k) , where V(e G)=V and E(e G)=E′∩V 2 , and thus, by Fact 2.1, has a (regular) refutation π of length at most L . Removing edges from a graph only introduces additional edge axioms (2a) in the corresponding formula, therefore Clique∗(e G,k) ⊆ Clique∗(G,k) and π is a valid refutation of Clique∗(G,k) as well. □ It was shown in [ 6 ] that the k -clique formula of a complete (k− 1 ) - partite graph on n vertices has a regular resolution refutation of length 2 knO(1) , although the regularity is not stressed in that paper. Since it is instructive to see how this refutation is constructed in this framework, we give a self-contained proof. Proposition 3.3 ([ 6 , Proposition 5.3]). If G is a (k− 1 ) -colourable graph on n vertices, then Clique∗(G,k) has a regular resolution refutation of length at most 2kk2n2. Proof. Let V=V(G) and let V1Û ∪V2Û ∪. . . Û ∪V(k−1) be a partition of V into colour classes. Define the graph G′=(V,E′) where the edge set E′ has an edge between any pair of vertices belonging to two different colour classes. Clearly G is a subgraph of G′ . Observe that any clique R in G′ has at most one vertex in each colour class, and that the common neighbours of R are all the vertices in the colour classes not touched by R. Therefore, there is a one-to-one correspondence between the members of I(G′) and the subsets of [k− 1 ] . By Proposition 3.1 there is a read-once branching program for the falsified clause search problem on formula Clique∗(G′,k) of size at most 2 kk2n2 . This read-once branching program corresponds to a regular resolution refutation of Clique∗(G′,k) of the same size. By Fact 3.2 there must be a regular resolution refutation of size at most 2 kk2n2 for Clique∗(G,k)as well. □ Next we generalize Proposition 3.3 to graphs G that have a homomorphism to a k-clique free graph H. Proposition 3.4. If G is a graph on n vertices that has a homomorphism into a k -clique free graph H on m vertices, then Clique∗(G,k) has a regular resolution refutation of length at most mkk2n2. Proof. Fix a homomorphism h : V(G) →V(H) and an ordering u1, . . . , um of the vertices of H . Let V1Û ∪V2Û ∪. . . Û ∪Vm be the partition of V(G) such that Vi is the set of vertices of G mapped to ui by h . We define the graph G′=(V,E′)where E′=Ø {ui,uj}∈E(H) Vi×Vj,(5) that is, G′ is a blown up version of H that contains G as a subgraph. To prove our result we note that, by Proposition 3.1, there is a readonce branching program for the falsified clause search problem on Clique∗(G′,k) —and hence also a regular resolution refutations of the same formula—of size at most |I(G′)| ·k2n2 . This implies that, by Fact 3.2, there is a regular resolution refutation of Clique∗(G,k) of at most the same size. To conclude the proof it remains only to show that |I(G′)| ≤mk . By construction, h maps injectively a clique R⊆V(G′) into a clique RH⊆V(H) of the same size. Moreover, note that if U=b N(RH) , then b N(R)=∪ui∈UVi . Therfore, for any clique R′⊆V(G′) that is mapped by h to RH it holds that b N(R)=b N(R′) , i.e., b N(R′) is completely characterized by the clique in H it is mapped to. Thus I(G) has at most one element for each clique in H and we have that |I(G′)| =|I(H)| . Finally, note that |I(H)| ≤mk since, being k -clique free, Hcannot have more than mkcliques. □ 4 RANDOM GRAPHS ARE HARD The main result of this paper is an average case lower bound of nΩ(k) for regular resolution for the k -clique problem. As we saw in Section 2, the k -clique problem can be encoded in different ways and depending on the preferred formula the range of k for which we can obtain a lower bound differs. In this section we present a summary of our results for the different encodings. Theorem 4.1. For any real constant ϵ> 0, any sufficiently large integer n , any positive integer k≤n1/4−ϵ , and any real ξ> 1, if G∼G(n,n−2ξ/(k−1)) is an Erdős-Rényi random graph, then, with probability at least 1 −exp(−√n) , any regular resolution refutation of Cliqueblock(G,k)has length at least nΩ(k/ξ2). The parameter ξ determines the density of the graph: the larger ξ the sparser the graph and the problem of determining whether G contains a k -clique becomes easier. For constant ξ , where the edge probability is somewhat close to the threshold for containing a k -clique, the theorem yields a nΩ(k) lower bound which is tight up to the multiplicative constant in the exponent. The lower bound decreases smoothly with the edge density and is non-trivial for ξ=o(√k). A problem which is closely related to the problem we consider is that of distinguishing a random graph sampled from G(n,p) from a random graph from the same distribution with a planted k -clique. The most studied setting is when p= 1 / 2. In this scenario the problem can be solved in polynomial time with high probability for k≈√n [ 1 , 20 ]. It is still an open problem whether there exists a polynomial time algorithm solving this problem for logn≪ k≪√n . For G∼G(n, 1 / 2 ) , Theorem 4.1 implies that to refute Cliqueblock(G,k) asymptotically almost surely regular resolution requires nΩ(log n) size for k=O(logn) and super-polynomial size for k=o(log2n). An interesting question is whether Theorem 4.1 holds for larger values of k . We show that for the formula Clique(G,k) (recall that by Lemma 2.2 this encoding is easier for the purpose of lower bounds) we can prove the lower bound for k≤n1/2−ϵ as long as the edge density of the graph is close to the threshold for containing ak-clique. Theorem 4.2. For any real constant ϵ> 0, any sufficiently large integer n , any positive integer k , and any real ξ> 1such that kpξ≤ n1/2−ϵ , if G∼G(n,n−2ξ/(k−1)) is an Erdős-Rényi random graph, then, with probability at least 1 −exp(−√n) , any regular resolution refutation of Clique(G,k)has length at least nΩ(k/ξ2). In this extended abstract we prove Theorem 4.2 and we refer to the upcomming full-length version of this paper for the proof of Theorem 4.1. We note, however, that both proofs are very similar and having seen one it is an easy exercise to obtain the other. The proof of Theorem 4.2 is deferred to Section 6and is based on a general lower bound technique we develop in Section 5. 5 CLIQUE-DENSENESS IMPLIES HARDNESS In this section we define a combinatorial property of graphs, which we call clique-denseness, and prove that if a k-clique -free graph G is clique-dense with the appropriate parameters, then this implies a lower bound nΩ(k) on the length of any regular resolution refutation of the k-clique formula on G. In order to argue that regular resolution has a hard time certifying the k-clique -freeness of a graph G , one property that seems useful to have is that for every small enough clique in the graph there are many ways of extending it to a larger clique. In other words, if R⊆V forms a clique and R is small, we would like the common neighbourhood b NV(R) to be large. This motivates the following definitions. Definition 5.1 (Neighbour-dense set). Given a graph G=(V,E) and q,r∈R+ , a set W⊆V is q -neighbour-dense for R⊆V if b NW(R)≥q . We say that W is (r,q) -neighbour-dense if it is q -neigh- bour-dense for every R⊆Vof size |R| ≤ r. If W is an (r,q) -neighbour-dense set, then we know that any clique of size r can be extended to a clique of size r+ 1in at least q different ways by adding some vertex of W . Note, however, that the definition of (r,q) -neighbour-dense is more general than this since Ris not required to be a clique. We next define a more robust notion of neighbour-denseness. For some settings of r and q of interest to us it is too much to hope for a set W which is q -neighbour-dense for every R⊆V of size at most r . In this case we would still like to be able to find a “mostly neighbour-dense” set W in the sense that we can “localize” bad sets R⊆V of size |R| ≤ r , i.e., those for which W fails to be q-neighbour-dense. Definition 5.2 (Mostly neighbour-dense set). Given G=(V,E) and r′,r,q′,s∈R+ with r′≥r , a set W⊆V is (r′,r,q′,s) -mostly neighbour-dense if there exists a set S⊆V of size |S| ≤ s such that for every R⊆V with |R| ≤ r′ for which W is not q′ -neighbour- dense, it holds that |R∩S| ≥ r. In what follows, it might be helpful for the reader to think of r′ and r as linear in k and q and s as polynomial in n , where we also have that s≪q. Now we are ready to define a property of graphs that makes it hard for regular resolution to certify that graphs with this property, but without k-cliques, are indeed k-clique-free. Definition 5.3 (Clique-dense graph). Given k∈N+ and t,s,ε∈R+, 1 ≤t≤k , we say that a graph G=(V,E) is (k,t,s,ε) -clique-dense if there exist r,q∈R+,r≥4k/t2, such that (1) Vis (tr,tq)-neighbour-dense, and (2) every (r,q) -neighbour-dense set W⊆V is (tr,r,q′,s) -mostly neighbour-dense for q′=3εks1+εlogs. Theorem 5.4. Given k∈N+ and t,s,ε∈R+ if the graph G is (k,t,s,ε) -clique-dense, then every regular resolution refutation of the CNF formula Clique(G,k)has length at least 1 √2sεk/t2. The value of q′ in Definition 5.3 is tailored so that Theorem 4.2 holds for k≪n1/2 on graphs with edge density close to the threshold for having a k -clique. Setting q′=εrs1+εlogs and making the necessary modifications in the proof would yield Theorem 4.2 for a larger range of edge densities but only for k≪n2/5. We will spend the rest of this section establishing Theorem 5.4. Fix r,q∈R+ witnessing that G is (k,t,s,ε) -clique-dense as per Definition 5.3. We first note that we can assume that tr ≤k since otherwise, by property 1of Definition 5.3, G contains a k -clique and the theorem follows immediately. By the discussion in Section 2it is sufficient to consider read-once branching programs, since they are equivalent to regular resolution refutations, and so in what follows this is the language in which we will phrase our lower bound. Thus, for the rest of this section let P be an arbitrary, fixed read-once branching program that solves the falsified clause search problem for Clique(G,k) . We will use the convention of referring to “vertices” of the graph G and “nodes” of the branching program Pto distinguish between the two. Recall that for a node a of P , β(a) denotes the maximal partial assignment that is contained in any assignment σ such that the path path(σ) passes through a . For any partial assignment β we write β1 to denote the partial assignment that contains exactly the variables that are set to 1in β . Clearly, if β falsifies an edge axiom or a functionality axiom, then so does β1 . Furthermore, for any β′⊆β1 , if β′ falsifies an edge axiom or a functionality axiom, so does β1 . We will use this monotonicity property of partial assignments throughout the proof. For each node a of P and each index i∈ [k] we define two sets of vertices V0 i(a)={v∈V|β(a)sets xv,ito 0}(6a) V1 i(a)={v∈V|β(a)sets xv,ito 1}(6b) of G . Observe that for β=β(a) the set of vertices referenced by variables in β1is ÐiV1 i(a). Intuitively, one can think of V0 i(a) and V1 i(a) as the sets of vertices v for which the variable xv,i is assigned 0and 1, respectively, that are guaranteed to be “remembered” at the node a (in the language of resolution, they correspond to negative and positive occurrences of variables in the clause Da associated with the node a ). Other assignments to variables xu,i for u<V0 i(a)∪V1 i(a) encountered along some path to a have been “forgotten” and may not be queried any more on any path starting at a . Formally, we say that a variable xv,i is forgotten at a if there is a path from the source of P to a passing through a node b where xv,i is queried, but v is not in V0 i(a) nor in V1 i(a) . Furthermore, we say index i is forgotten at a if for some vertex v the variable xv,i is forgotten at a . Of utter importance is the fact that these notions are persistent: if a variable or an index is forgotten at a node a , then it will also be the case for any node reachable from a by a path. We say that a path in P ends in the i th clique axiom if the clause that labels its last node is the clique axiom (2b) of Clique(G,k) with index i . The above observation implies that the index i cannot be forgotten at any node along such a path. We establish our lower bound via a bottleneck counting argument for paths in P . To this end, let us define a distribution D over paths in P by the following random process. The path starts at the source and ends whenever it reaches a sink of P . At an internal node a with successor nodes a0 and a1 , reached by edges labelled 0 and 1respectively, the process proceeds as follows. (1) If X(a)=xu,i and i is forgotten at a then the path proceeds via the edge labelled 0to a0. (2) If X(a)=xu,i and β(a) ∪ {xu,i= 1 } falsifies an edge axiom (2a) or a functionality axiom (2c) , then the path proceeds to a0. (3) Otherwise, an independent (rs−(1+ε)/ 2e k) -biased coin is tossed with outcome γ∈ { 0 , 1 } and the random path proceeds to aγ . We say that in cases (1) and (2) the answer to the query X(a) is forced. Note that any path α in the support of D must end in a clique axiom since α does not falsify any edge or functionality axiom by construction. Moreover, a property that will be absolutely crucial is that only answers 0can be forced—answers 1are always the result of a coin flip. Claim 5.5. Every path in the support of D sets at most k variables to 1. Proof. Let α be a path in the support of D . We argue that for each i∈ [k] at most one variable with second index i is set to 1 on α . Let a and b be two nodes that appear in this order in α . If for some i∈ [k] , and for some u,v∈V , xu,i is set to 1by α at node a and xv,i is queried at b , then v,u by regularity and, by definition of D , the answer to query xv,i will be forced to 0, either to avoid violating a functionality or an edge axiom, or because i is forgotten at b.□ Let us call a pair (a,b) of nodes of P useful if there exists an index i such that V1 i(b)=∅ , i is not forgotten at b , and the set V0 i(b)\V0 i(a) is (r,q) -neighbour-dense. For each useful pair (a,b) , let i(a,b) be an arbitrary but fixed index witnessing that (a,b) is useful. A path is said to usefully traverse a useful pair (a,b) if it goes through a and b in that order and sets at most ⌈k/t⌉ variables to 1between aand b(with aincluded and bexcluded). As already mentioned, the proof of Theorem 5.4 is based on a bottleneck counting argument in the spirit of [ 12 ], with the twist that we consider pairs of bottleneck nodes. To establish the theorem we make use of the following two lemmas which will be proven subsequently. Lemma 5.6. Every path in the support of D usefully traverses a useful pair. Lemma 5.7. For every useful pair (a,b) , the probability that a random α chosen from D usefully traverses (a,b) is at most 2 s−εr/2 . Combining the above lemmas, it is immediate to prove Theorem 5.4. By Lemma 5.6 the probability that a random path α sampled from D usefully traverses some useful pair is 1. By Lemma 5.7, for any fixed useful pair (a,b) , the probability that a random α usefully traverses (a,b) is at most 2 s−εr/2 . By a standard union bound argument, it follows that the number of useful pairs is at least 1 2sεr/2 , so the number of nodes in P cannot be smaller than 1 √2sεr/4≥1 √2sεk/t2. To conclude the proof it remains only to establish Lemmas 5.6 and 5.7. Proof of Lemma 5.6. Consider any path in the support of D . By the definition of our random process this path ends in the i∗ th clique axiom for some i∗∈ [k] . By Claim 5.5, the path sets at most k variables to 1and hence we can split it into t pieces by nodes a0,a1, . . . , at ( a0 is the source, at the sink) so that between aj and aj+1 at most ⌈k/t⌉ variables are set to 1. It remains to prove that for at least one j∈ [t]the set Wj=V0 i∗(aj)\V0 i∗(aj−1)(7) is (r,q) -neighbour-dense. Note that this will prove Lemma 5.6 since by construction (aj−1,aj) is then a pair that is usefully traversed by the path. Towards contradiction, assume instead that no Wj is (r,q) -neigh- bour-dense, i.e., that for all j∈ [t] there exists a set of vertices Rj⊆V with |Rj| ≤ r such that b NWj(Rj)≤q . Let R=Ðj∈[t]Rj . Since the path ends in the i∗ th clique axiom we have V0 i∗(at)=V , and since i∗ is not forgotten along the path, it holds that V0 i∗(aj−1) ⊆ V0 i∗(aj) for each j∈ [t] . It follows that the sets W1, . . . ,Wt in (7) form a partition of V, and therefore b NV(R)=Õ j∈[t]b NWj(R)≤Õ j∈[t]b NWj(Rj)≤tq .(8) Since |R| ≤ Íj∈[t]|Rj| ≤ tr this contradicts the assumption that V is (tr,tq)-neighbour-dense. Lemma 5.6 follows. □ Proof of Lemma 5.7. Fix a useful pair (a,b) . Let Edenote the event that a random path sampled from D usefully traverses (a,b) . Let i∗=i(a,b) , V1(a)=Ðj∈[k]V1 j(a) , and W=V0 i∗(b) \V0 i∗(a) . Notice that W is guaranteed to be (r,q) -neighbour-dense by our definition of i(a,b) . Since G is (k,t,s,ε) -clique-dense by assumption, this implies that W is (tr,r,q′,s) -mostly neighbour-dense, and we let S be the set that witnesses this as per Definition 5.2. We bound the probability of the event Eby a case analysis based on the size of the set V1(a) . We remark that all probabilities in the calculations that follow are over the choice of α∼D. Case 1 (|V1(a)| >r/ 2 ) : In this case, we simply prove that already the probability of reaching a is small. By definition of |V1(a)| , we have that |β1(a)| =|V1(a)| . Recall that every answer 1is necessarily the result of a (rs−(1+ε)/ 2e k) -biased coin flip, and that all these decisions are irreversible. That is, if a path ever decides to set a variable in V1(a) to 0, then its case is lost and it is guaranteed to miss a . Thus we can upper bound the probability of the event Eby the probability that a random α passes through a , and, in particular, by the probability of setting all variables in β1(a)to 1as follows: Pr[E] ≤ Pr[αpasses through a](9) ≤rs−(1+ε)/2ek|β1(a)| (10) ≤s−ε|β1(a)| (11) =s−ε|V1(a)| (12) ≤2s−εr/2,(13) where for (11) we use the fact that r≤k , which follows from tr ≤k and t≥1. Case 2 (|V1(a)| ≤ r/ 2 ) : For every path α , let R(α) denote the set of vertices u for which the path α sets some variable xu,i to 1 at some node between a and b (with a included and b excluded); note that R(α)=∅ if α does not go through a and b , and that |R(α)| ≤ ⌈k/t⌉ for all paths α that satisfy the event E. For the sets R0={R:|R| ≤ ⌈k/t⌉and b NW(R∪V1(a))<q′}(14a) R1={R:|R| ≤ ⌈k/t⌉and b NW(R∪V1(a))≥q′}(14b) we have that Pr[E]=Pr[Eand R(α) ∈ R0]+Pr[Eand R(α) ∈ R1].(15) The first term in (15) is bounded from above by the probability of R(α) ∈ R0 . Note that |R| ≤ ⌈k/t⌉ ≤ 2 k/t≤rt/ 2(since r≥ 4 k/t2 ) for R∈ R0 . Hence we have |R∪V1(a)| ≤ rt/ 2 +r/ 2 ≤rt and therefore |(R∪V1(a))∩S| ≥ r by the choice of S . Thus, the probability of R(α) ∈ R0 is bounded by the probability that |R(α)∩S| ≥ r/ 2 since |V1(a)| ≤ r/ 2. But since S is small, we can now apply the union bound and conclude that Pr[Eand R(α) ∈ R0] ≤ Pr[R(α) ∈ R0](16) ≤Pr[|R(α)∩S| ≥ r/2](17) ≤|S|k r/2 rs−(1+ε) 2ek!r/2 (18) ≤2e|S|k rr/2 rs−(1+ε) 2ek!r/2 (19) ≤s−εr/2.(20) We now bound the second term in (15) . First note that, by definition of W , if α is a path that passes through a and b in this order, then all variables xu,i∗ with u∈W must be set to 0in α at some node between a and b . For each path in the support of D that passes through a and b , some of the variables xu,i∗ with u∈W will be set to zero as a result of a coin flip and others will be forced choices. Fix a path α contributing to the second term in (15) . We claim that along this path at least q′ variables xu,i∗(u∈W) are set to 0 as a result of a coin flip. Indeed, since V1 i∗(b)=∅ and i∗ is not forgotten at b , by the monotonicity property the same holds for every node along α before b . This implies that the answer to a query of the form xu,i∗(u∈W) made along α cannot be forced by neither item (1) (forgetfulness) in the definition of D nor by a functionality axiom. Moreover, since V1(c) ⊆ R(α)∪V1(a) for any node c on the path α between a and b , it holds that all variables xu,i∗ with u∈b NW(R(α)∪V1(a)) can not be forced to 0 by an edge axiom either. Since there are at least q′ of them, this proves the claim. Now the analysis of the second term in (15) is completed by the same Markov chain argument as in Case 1 above (noting that irreversibility of decisions still takes place): Pr[Eand R(α) ∈ R1] ≤Pr[αflips ≥q′coins and gets all 0s](21) ≤1−rs−(1+ε)/2ekq′(22) ≤s−εr/2.(23) Adding (20) and (23) we obtain the lemma. □ 6 RANDOM GRAPHS ARE CLIQUE-DENSE In this section we show that asymptotically almost surely an Erdős- Rényi random graph G∼G(n,p) is (k,t,s,ε) -clique-dense for the right choice of parameters. Theorem 6.1. For any real constant ε∈ ( 0 , 1 / 2 ) , any sufficiently large integer n , any positive integer k and any real ξ> 1such that kpξ≤n1/2−ε , if G∼G(n,n−2ξ/(k−1)) is an Erdős-Rényi random graph then with probability at least 1 −exp(−√n) it holds that G is (k,t,s,ε)-clique-dense with t=64ξ/εand s=(n/ξ)1/2. As a corollary of Theorem 5.4 and Theorem 6.1 we obtain Theorem 4.2, the main result of this paper. Proof of Theorem 4.2. Clearly t≥ 128 ≥ 1as required by Definition 5.3. We can also assume w.l.o.g. that t≤k since otherwise k/ξ2≤ 64 /(ξϵ) ≤ O( 1 ) and the bound becomes trivial. By plugging in the parameters given by Theorem 6.1 to Theorem 5.4 we immediately get the stated lower bound on the length of any regular refutation πof Clique(G,k) |π| ≥ 1 √2sεk/t2≥nΩ(k/ξ2),(24) for which we have to note that s≥n1/4 since ξ≤t≤k≤n1/2 . □ We will spend the rest of this section proving Theorem 6.1. Let δ= 2 ξ/(k− 1 ) . We show that, with probability at least 1 − e −√n , the random graph G is (k,t,s,ε) -clique-dense for parameters as in the statement of the theorem, r=4k/t2and q=n1−tδr 4t. Recall that q′= 3 εks1+εlogs . Let us argue that these parameters satisfy constraints tδr≤ε 6,(25) tr logn≤n1−tδr 32 ·logn n1/2,(26) qn−tδrs 16tr ≥n1+2ε/3 28,(27) q′≤qn−tδr 4·3·29logn nε/6,(28) tr ≤q 2,(29) which will be used further on in the proof. As a first step note that for k≥4 tδr=8ξk t(k−1)≤ε 6,(30) and hence (25) holds. Equation (26) follows from the chain of inequalities tr logn=4klogn t≤n1/2−εlogn 32 ≤n1−tδr 32 ·logn n1/2.(31) To obtain (27) observe that qn−tδrs 16tr =n1−2tδr+1/2 28kξ1/2≥n1−2tδr+ε 28≥n1+2ε/3 28.(32) To see that (28) holds, note that q′=3εks1+εlogs(33) ≤3εkn(1+ε)/2logn 2ξ1/2(34) =3·25·kξ1/2n(1+ε)/2logn t(35) ≤3·29·n1−ε/2logn 16t(36) ≤qn−tδr 4·3·29logn nε/6.(37) Finally, for (29), we just observe that tr =4k t≤4k2 t2≤n1−2ε 16t≤q 2,(38) where we use that k≥tand t≥64.