Atserias and Müller (JACM, 2020) proved that for every unsatisfiable CNF formula $\varphi$, the formula $\operatorname{Ref}(\varphi)$ stating that “$\varphi$ has small Resolution refutations"-does not have subexponential-size Resolution refutations. Conversely, when $\varphi$ is satisfiable, Pudlák (TCS, 2003) showed how to construct a polynomial-size Resolution refutation of $\operatorname{REF}(\varphi)$ given a satisfying assignment of $\varphi$. A question that had remained open is: do all short Resolution refutations of $\operatorname{Ref}(\varphi)$ explicitly leak a satisfying assignment of $\varphi$?We answer this question affirmatively by providing a polynomial-time algorithm that extracts a satisfying assignment for $\varphi$ given any short Resolution refutation of $\operatorname{REF}(\varphi)$. The algorithm follows from a new feasibly constructive proof of the Atserias-Müller lower bound, formalizable in Cook’s theory PV1of bounded arithmetic. This implies that Extended Frege can efficiently prove (a suitable formalization of the statement) that automating Resolution is NP-hard.Motivated by this algorithm, we introduce a new metacomputational problem concerning Resolution lower bounds: the Proof Analysis Problem (PAP). For a fixed proof system Q, the Proof Analysis Problem for Q asks, given a CNF formula $\varphi$ and a Q-proof of a Resolution lower bound for $\varphi$, encoded as $\neg \boldsymbol{REF}(\varphi)$, whether $\varphi$ is satisfiable. In contrast to the Proof Analysis Problem for Resolution, which is in P, we prove that PAP for Extended Frege (EF) is NP-complete. In particular, EF can prove Resolution lower bounds on satisfiable formulas without necessarily revealing a satisfying assignment.Our results yield new insights into proof search and the meta-mathematics of Resolution lower bounds: (i) for every proof system that simulates EF as well as for Resolution, the system is (weakly) automatable if and only if it can be (weakly) automated exclusively on formulas stating Resolution lower bounds; (ii) we provide explicit Ref formulas that are exponentially hard for bounded-depth Frege systems; and (iii) for every strong enough theory of arithmetic T we construct explicit unsatisfiable CNF formulas that are exponentially hard for Resolution but for which T cannot prove even a quadratic Resolution lower bound. This latter result applies to arbitrarily strong theories like PA or ZFC, and does not require any complexity-theoretic assumptions.

The Schwartz-Zippel Lemma states that if a low-degree multivariate polynomial with coefficients in a field is not zero everywhere in the field, then it has few roots on every finite subcube of the field. This fundamental fact about multivariate polynomials has found many applications in algorithms, complexity theory, coding theory, and combinatorics. We give a new proof of the lemma that offers some advantages over the standard proof. First, the new proof is more constructive than previously known proofs. For every given side-length of the cube, the proof constructs a polynomial-time computable and polynomial-time invertible surjection onto the set of roots in the cube. The domain of the surjection is tight, thus showing that the set of roots on the cube can be compressed. Second, the new proof can be formalised in Buss’ bounded arithmetic theory S21 for polynomial-time reasoning. One consequence of this is that the theory S21 + dWPHP(PV) for approximate counting can prove that the problem of verifying polynomial identities (PIT) can be solved by polynomial-size circuits. The same theory can also prove the existence of small hitting sets for any explicitly described class of polynomials of polynomial degree. To complete the picture we show that the existence of such hitting sets is equivalent to the surjective weak pigeonhole principle dWPHP(PV), over the theory S21. This is a contribution to a line of research studying the reverse mathematics of computational complexity. One consequence of this is that the problem of constructing small hitting sets for such classes is complete for the class APEPP of explicit construction problems whose totality follows from the probabilistic method. This class is also known and studied as the class of Range Avoidance Problems.

The interplay between local consistency and global consistency has been the object of study in several different areas, including probability theory, relational databases, and quantum information. For relational databases, Beeri, Fagin, Maier, and Yannakakis showed that a database schema is acyclic if and only if it has the local-to-global consistency property for relations, which means that every collection of pairwise consistent relations over the schema is globally consistent. More recently, the same result has been shown under bag semantics. In this article, we carry out a systematic study of local versus global consistency for relations over positive commutative monoids, which is a common generalization of ordinary relations and bags. Let \(\mathbb {K}\) be an arbitrary positive commutative monoid. We begin by showing that acyclicity of the schema is a necessary condition for the local-to-global consistency property for \(\mathbb {K}\) -relations to hold. Unlike the case of ordinary relations and bags, however, we show that acyclicity is not always sufficient. Then, we characterize the positive commutative monoids for which acyclicity is both necessary and sufficient for the local-to-global consistency property to hold. This characterization involves a combinatorial property of monoids, which we call the transportation property . We then identify several different classes of monoids that possess the transportation property. As our final contribution, we introduce a modified notion of local consistency of \(\mathbb {K}\) -relations, which we call pairwise consistency up to the free cover . We prove that, for all positive commutative monoids \(\mathbb {K}\) , even those without the transportation property, acyclicity is both necessary and sufficient for every family of \(\mathbb {K}\) -relations that is pairwise consistent up to the free cover to be globally consistent.

The interplay between local consistency and global consistency has been the object of study in several different areas, including probability theory, relational databases, and quantum information. For relational databases, Beeri, Fagin, Maier, and Yannakakis showed that a database schema is acyclic if and only if it has the local-to-global consistency property for relations, which means that every collection of pairwise consistent relations over the schema is globally consistent. More recently, the same result has been shown under bag semantics. In this paper, we carry out a systematic study of local vs. global consistency for relations over positive commutative monoids, which is a common generalization of ordinary relations and bags. Let K be an arbitrary positive commutative monoid. We begin by showing that acyclicity of the schema is a necessary condition for the local-to-global consistency property for K-relations to hold. Unlike the case of ordinary relations and bags, however, we show that acyclicity is not always sufficient. After this, we characterize the positive commutative monoids for which acyclicity is both necessary and sufficient for the local-to-global consistency property to hold; this characterization involves a combinatorial property of monoids, which we call the transportation property. We then identify several different classes of monoids that possess the transportation property. As our final contribution, we introduce a modified notion of local consistency of K-relations, which we call pairwise consistency up to the free cover. We prove that, for all positive commutative monoids K, even those without the transportation property, acyclicity is both necessary and sufficient for every family of K-relations that is pairwise consistent up to the free cover to be globally consistent.

We prove the first unconditional consistency result for superpolynomial circuit lower bounds with a relatively strong theory of bounded arithmetic. Namely, we show that the theory ‍V20 is consistent with the conjecture that ‍NEXP ‍⊈ ‍P/poly, i.e., some problem that is solvable in non-deterministic exponential time does not have polynomial size circuits. We suggest this is the best currently available evidence for the truth of the conjecture. Additionally, we establish a magnification result on the hardness of proving circuit lower bounds.

Abstract. The ellipsoid method is an algorithm that solves the (weak) feasibility and linear optimization problems for convex sets by making oracle calls to their (weak) separation problem. We observe that the previously known method for showing that this reduction can be done in fixed-point logic with counting (FPC) for linear and semidefinite programs applies to any family of explicitly bounded convex sets. We further show that the exact feasibility problem for semidefinite programs is expressible in the infinitary version of FPC. As a corollary, we get that, for the graph isomorphism problem, the Lasserre/sums-of-squares semidefinite programming hierarchy of relaxations collapses to the Sherali–Adams linear programming hierarchy, up to a small loss in the degree.

Proofs in propositional logic are typically presented as trees of derived formulas or, alternatively, as directed acyclic graphs of derived formulas. This distinction between tree-like vs. dag-like structure is particularly relevant when making quantitative considerations regarding, for example, proof size. Here we analyze a more general type of structural restriction for proofs in rule-based proof systems. In this definition, proofs are directed graphs of derived formulas in which cycles are allowed as long as every formula is derived at least as many times as it is required as a premise. We call such proofs “circular”. We show that, for all sets of standard inference rules with single or multiple conclusions, circular proofs are sound. We start the study of the proof complexity of circular proofs at Circular Resolution, the circular version of Resolution. We immediately see that Circular Resolution is stronger than dag-like Resolution since, as we show, the propositional encoding of the pigeonhole principle has circular Resolution proofs of polynomial size. Furthermore, for derivations of clauses from clauses, we show that Circular Resolution is, surprisingly, equivalent to Sherali-Adams, a proof system for reasoning through polynomial inequalities that has linear programming at its base. As corollaries we get: (1) polynomial-time (LP-based) algorithms that find Circular Resolution proofs of constant width, (2) examples that separate Circular from dag-like Resolution, such as the pigeonhole principle and its variants, and (3) exponentially hard cases for Circular Resolution. Contrary to the case of Circular Resolution, for Frege we show that circular proofs can be converted into tree-like proofs with at most polynomial overhead.

We study the power of the bounded-width consistency algorithm in the context of the fixed-template Promise Constraint Satisfaction Problem (PCSP). Our main technical finding is that the template of every PCSP that is solvable in bounded width satisfies a certain structural condition implying that its algebraic closure-properties include weak near unanimity polymorphisms of all large arities. While this parallels the standard (non-promise) CSP theory, the method of proof is quite different and applies even to the regime of sublinear width. We also show that, in contrast with the CSP world, the presence of weak near unanimity polymorphisms of all large arities does not guarantee solvability in bounded width. The separating example is even solvable in the second level of the Sherali-Adams (SA) hierarchy of linear programming relaxations. This shows that, unlike for CSPs, linear programming can be stronger than bounded width. A direct application of these methods also show that the problem of q-coloring p-colorable graphs is not solvable in bounded or even sublinear width, for any two constants p and q such that 3 ≤ p ≤ q. Turning to algorithms, we note that Wigderson's algorithm for -coloring 3-colorable graphs with n vertices is implementable in width 4. Indeed, by generalizing the method we see that, for any ∊ > 0 smaller than 1/2, the optimal width for solving the problem of O(n∊)-coloring 3-colorable graphs with n vertices lies between n1–3∊ and n1–2∊. The upper bound gives a simple exp(Θ(n1–2∊ log(n)))-time algorithm that, asymptotically, beats the straightforward exp(Θ(n1–∊)) bound that follows from partitioning the graph into O(n∊) many independent parts each of size O(n1–∊).

A classical result by Lovász asserts that two graphs G and H are isomorphic if and only if they have the same left profile, that is, for every graph F, the number of homomorphisms from F to G coincides with the number of homomorphisms from F to H. Dvorák and later on Dell, Grohe, and Rattan showed that restrictions of the left profile to a class of graphs can capture several different relaxations of isomorphism, including equivalence in counting logics with a fixed number of variables (which contains fractional isomorphism as a special case) and co-spectrality (i.e., two graphs having the same characteristic polynomial). On the other side, a result by Chaudhuri and Vardi asserts that isomorphism is also captured by the right profile, that is, two graphs G and H are isomorphic if and only if for every graph F, the number of homomorphisms from G to F coincides with the number of homomorphisms from H to F. In this paper, we embark on a study of the restrictions of the right profile by investigating relaxations of isomorphism that can or cannot be captured by restricting the right profile to a fixed class of graphs. Our results unveil striking differences between the expressive power of the left profile and the right profile. We show that fractional isomorphism, equivalence in counting logics with a fixed number of variables, and co-spectrality cannot be captured by restricting the right profile to a class of graphs. In the opposite direction, we show that chromatic equivalence cannot be captured by restricting the left profile to a class of graphs, while, clearly, it can be captured by restricting the right profile to the class of all cliques.

Since the early days of relational databases, it was realized that acyclic hypergraphs give rise to database schemas with desirable structural and algorithmic properties. In a by-now classical paper, Beeri, Fagin, Maier, and Yannakakis established several different equivalent characterizations of acyclicity; in particular, they showed that the sets of attributes of a schema form an acyclic hypergraph if and only if the local-to-global consistency property for relations over that schema holds, which means that every collection of pairwise consistent relations over the schema is globally consistent. Even though real-life databases consist of bags (multisets), there has not been a study of the interplay between local consistency and global consistency for bags. We embark on such a study here and we first show that the sets of attributes of a schema form an acyclic hypergraph if and only if the local-to-global consistency property for bags over that schema holds. After this, we explore algorithmic aspects of global consistency for bags by analyzing the computational complexity of the global consistency problem for bags: given a collection of bags, are these bags globally consistent? We show that this problem is in NP, even when the schema is part of the input. We then establish the following dichotomy theorem for fixed schemas: if the schema is acyclic, then the global consistency problem for bags is solvable in polynomial time, while if the schema is cyclic, then the global consistency problem for bags is NP-complete. The latter result contrasts sharply with the state of affairs for relations, where, for each fixed schema, the global consistency problem for relations is solvable in polynomial time.

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 show that if a system of degree-$k$ polynomial constraints on~$n$ Boolean variables has a Sums-of-Squares (SOS) proof of unsatisfiability with at most~$s$ many monomials, then it also has one whose degree is of the order of the square root of~$n \log s$ plus~$k$. A similar statement holds for the more general Positivstellensatz (PS) proofs. This establishes size-degree trade-offs for SOS and PS that match their analogues for weaker proof systems such as Resolution, Polynomial Calculus, and the proof systems for the LP and SDP hierarchies of Lovász and Schrijver. As a corollary to this, and to the known degree lower bounds, we get optimal integrality gaps for exponential size SOS proofs for sparse random instances of the standard NP-hard constraint optimization problems. We also get exponential size SOS lower bounds for Tseitin and Knapsack formulas. The proof of our main result relies on a zero-gap duality theorem for pre-ordered vector spaces that admit an order unit, whose specialization to PS and SOS may be of independent interest.

We show that the problem of finding a Resolution refutation that is at most polynomially longer than a shortest one is NP-hard. In the parlance of proof complexity, Resolution is not automatizable unless P = NP. Indeed, we show that it is NP-hard to distinguish between formulas that have Resolution refutations of polynomial length and those that do not have subexponential length refutations. This also implies that Resolution is not automatizable in subexponential time or quasi-polynomial time unless~NP is included in SUBEXP or QP, respectively.

We consider families of symmetric linear programs (LPs) that decide a property of graphs (or other relational structures) in the sense that, for each size of graph, there is an LP defining a polyhedral lift that separates the integer points corresponding to graphs with the property from those corresponding to graphs without the property. We show that this is equivalent, with at most polynomial blow-up in size, to families of symmetric Boolean circuits with threshold gates. In particular, when we consider polynomial-size LPs, the model is equivalent to definability in a non-uniform version of fixed-point logic with counting (FPC). Known upper and lower bounds for FPC apply to the non-uniform version. In particular, this implies that the class of graphs with perfect matchings has polynomial-size symmetric LPs, while we obtain an exponential lower bound for symmetric LPs for the class of Hamiltonian graphs. We compare and contrast this with previous results (Yannakakis 1991), showing that any symmetric LPs for the matching and TSP polytopes have exponential size. As an application, we establish that for random, uniformly distributed graphs, polynomial-size symmetric LPs are as powerful as general Boolean circuits. We illustrate the effect of this on the well-studied planted-clique problem.

Schaefer introduced a framework for generalized satisfiability problems on the Boolean domain and characterized the computational complexity of such problems. We investigate an algebraization of Schaefer's framework in which the Fourier transform is used to represent constraints by multilinear polynomials in a unique way. This representation of constraints gives rise to a relaxation of the notion of satisfiability in which the values to variables are linear operators on some Hilbert space. For constraints given by a system of linear equations over the two-element field, earlier work in the foundations of quantum mechanics has shown that there are systems that have no solutions in the Boolean domain, but have solutions via operator assignments on some finite-dimensional Hilbert space. Our main result is a complete characterization of the classes of Boolean relations for which there is a gap between satisfiability in the Boolean domain and the relaxation of satisfiability via operator assignments.

Abstract We consider the hardness of approximation of optimization problems from the point of view of definability. For many $\textrm{NP}$-hard optimization problems it is known that, unless $\textrm{P} = \textrm{NP} $, no polynomial-time algorithm can give an approximate solution guaranteed to be within a fixed constant factor of the optimum. We show, in several such instances and without any complexity theoretic assumption, that no algorithm that is expressible in fixed-point logic with counting (FPC) can compute an approximate solution. Since important algorithmic techniques for approximation algorithms (such as linear or semidefinite programming) are expressible in FPC, this yields lower bounds on what can be achieved by such methods. The results are established by showing lower bounds on the number of variables required in first-order logic with counting to separate instances with a high optimum from those with a low optimum for fixed-size instances.

We analyze how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, and semialgebraic proof systems, the classical constructions of pp-interpretability, homomorphic equivalence, and addition of constants to a core preserve the proof complexity of the CSP. As a result, for those proof systems, the classes of constraint languages for which small unsatisfiability certificates exist can be characterized algebraically. We illustrate our results by a gap theorem saying that a constraint language either has resolution refutations of constant width or does not have bounded-depth Frege refutations of subexponential size. The former holds exactly for the widely studied class of constraint languages of bounded width. This class is also known to coincide with the class of languages with refutations of sublinear degree in Sums of Squares and Polynomial Calculus over the real field, for which we provide alternative proofs. We then ask for the existence of a natural proof system with good behavior with respect to reductions and simultaneously small-size refutations beyond bounded width. We give an example of such a proof system by showing that bounded-degree Lovász-Schrijver satisfies both requirements. Finally, building on the known lower bounds, we demonstrate the applicability of the method of reducibilities and construct new explicit hard instances of the graph three-coloring problem for all studied proof systems.

We show that for no surface except for the plane does monadic second-order logic (MSO) have a zero-one-law - and not even a convergence law - on the class of (connected) graphs embeddable on the surface. In addition we show that every rational in [0,1] is the limiting probability of some MSO formula. This strongly refutes a conjecture by Heinig et al. (2014) who proved a convergence law for planar graphs, and a zero-one law for connected planar graphs, and also identified the so-called gaps of [0,1]: the subintervals that are not limiting probabilities of any MSO formula. The proof relies on a combination of methods from structural graph theory, especially large face-width embeddings of graphs on surfaces, analytic combinatorics, and finite model theory, and several parts of the proof may be of independent interest. In particular, we identify precisely the properties that make the zero-one law work on planar graphs but fail for every other surface.

The ellipsoid method is an algorithm that solves the (weak) feasibility and linear optimization problems for convex sets by making oracle calls to their (weak) separation problem. We observe that the previously known method for showing that this reduction can be done in fixed-point logic with counting (FPC) for linear and semidefinite programs applies to any family of explicitly bounded convex sets. We use this observation to show that the exact feasibility problem for semidefinite programs is expressible in the infinitary version of FPC. As a corollary we get that, for the graph isomorphism problem, the Lasserre/Sums-of-Squares semidefinite programming hierarchy of relaxations collapses to the Sherali-Adams linear programming hierarchy, up to a small loss in the degree.

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.

Homogenization is a powerful way of taming a class of finite structures with several interesting applications in different areas, from Ramsey theory in combinatorics to constraint satisfaction problems (CSPs) in computer science, through (finite) model theory. A few sufficient conditions for a class of finite structures to allow homogenization are known, and here we provide a necessary condition. This lets us show that certain natural classes are not homogenizable: 1) the class of locally consistent systems of linear equations over the two-element field or any finite Abelian group, and 2) the class of finite structures that forbid homomorphisms from a specific MSO-definable class of structures of treewidth two. In combination with known results, the first example shows that, up to pp-interpretability, the CSPs that are solvable by local consistency methods are distinguished from the rest by the fact that their classes of locally consistent instances are homogenizable. The second example shows that, for MSO-definable classes of forbidden patterns, treewidth one versus two is the dividing line to homogenizability.

We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n Ω( w ) . This shows that the simple counting argument that any formula refutable in width w must have a proof in size n O( w ) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. The lower bound does not extend all the way to Lasserre, however, since we show that there the formulas we study have proofs of constant rank and size polynomial in both n and w .

We study a natural variant of the implicational fragment of propositional logic. Its formulas are pairs of conjunctions of positive literals, related together by an implicational-like connective, the semantics of this sort of implication is defined in terms of a threshold on a conditional probability of the consequent, given the antecedent: we are dealing with what the data analysis community calls confidence of partial implications or association rules. Existing studies of redundancy among these partial implications have characterized so far only entailment from one premise and entailment from two premises. By exploiting a previously noted alternative view of this entailment in terms of linear programming duality, we characterize exactly the cases of entailment from arbitrary numbers of premises. As a result, we obtain decision algorithms of better complexity, additionally, for each potential case of entailment, we identify a critical confidence threshold and show that it is, actually, intrinsic to each set of premises and antecedent of the conclusion.

Abstract The relativized weak pigeonhole principle states that if at least 2n out of n2 pigeons fly into n holes, then some hole must be doubly occupied. We prove that every DNF-refutation of the CNF encoding of this principle requires size $2^{\left( {{\rm{log\ }}n} \right)^{3/2 - \varepsilon } } $ for every ε﹥0 and every sufficiently large n. By reducing it to the standard weak pigeonhole principle with 2n pigeons and n holes, we also show that this lower bound is essentially tight in that there exist DNF-refutations of size $2^{\left( {{\rm{log\ }}n} \right)^{O\left( 1 \right)} } $ even in R(log). For the lower bound proof we need to discuss the existence of unbalanced low-degree bipartite expanders satisfying a certain robustness condition.

We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size nΩ(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size nO(w)is essentially tight. Moreover, our lower bounds can be generalized to polynomial calculus resolution (PCR) and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. Our results do not extend all the way to Lasserre, however-the formulas we study have Lasserre proofs of constant rank and size polynomial in both n and w.

Kolaitis and Kopparty have shown that for any first-order formula with parity quantifiers over the language of graphs, there is a family of multivariate polynomials of constant-degree that agree with the formula on all but a 2 −Ω( n ) -fraction of the graphs with n vertices. The proof bounds the degree of the polynomials by a tower of exponentials whose height is the nesting depth of parity quantifiers in the formula. We show that this tower-type dependence is necessary. We build a family of formulas of depth q whose approximating polynomials must have degree bounded from below by a tower of exponentials of height proportional to q . Our proof has two main parts. First, we adapt and extend the results by Kolaitis and Kopparty that describe the joint distribution of the parities of the numbers of copies of small subgraphs in a random graph to the setting of graphs of growing size. Second, we analyze a variant of Karp's graph canonical labeling algorithm and exploit its massive parallelism to get a formula of low depth that defines an almost canonical pre-order on a random graph.

The ordering principle states that every finite linear order has a least element. We show that, in the relativized setting, the surjective weak pigeonhole principle for polynomial time functions does not prove a Herbrandized version of the ordering principle over T 1 2 . This answers an open question raised in Buss et al. [2012] and completes their program to compare the strength of Jeřábek's bounded arithmetic theory for approximate counting with weakened versions of it.

The relativized weak pigeonhole principle states that if at least 2n out of n2pigeons fly into n holes, then some hole must be doubly occupied. We prove that every DNF-refutation of the CNF encoding of this principle requires size 2((log n)3/2-ε) for every ϵ > 0 and every sufficiently large n. For its proof we need to discuss the existence of unbalanced low-degree bipartite expanders satisfying a certain robustness condition.

Tree-width is a well-studied parameter of structures that measures their similarity to a tree. Many important NP-complete problems, such as Boolean satisfiability (SAT), are tractable on bounded tree-width instances. In this paper we focus on the canonical PSPACE-complete problem QBF, the fully-quantified version of SAT. It was shown by Pan and Vardi [LICS 2006] that this problem is PSPACE-complete even for formulas whose tree-width grows extremely slowly. Vardi also posed the question of whether the problem is tractable when restricted to instances of bounded tree-width. We answer this question by showing that QBF on instances with constant tree-width is PSPACE-complete.

Relational joins are at the core of relational algebra, which in turn is the core of the standard database query language SQL. As their evaluation is expensive and very often dominated by the output size, it is an important task for database query optimizers to compute estimates on the size of joins and to find good execution plans for sequences of joins. We study these problems from a theoretical perspective, both in the worst-case model and in an average-case model where the database is chosen according to a known probability distribution. In the former case, our first key observation is that the worst-case size of a query is characterized by the fractional edge cover number of its underlying hypergraph, a combinatorial parameter previously known to provide an upper bound. We complete the picture by proving a matching lower bound and by showing that there exist queries for which the join-project plan suggested by the fractional edge cover approach may be substantially better than any join plan that does not use intermediate projections. On the other hand, we show that in the average-case model, every join-project plan can be turned into a plan containing no projections in such a way that the expected time to evaluate the plan increases only by a constant factor independent of the size of the database. Not surprisingly, the key combinatorial parameter in this context is the maximum density of the underlying hypergraph. We show how to make effective use of this parameter to eliminate the projections.

Two graphs with adjacency matrices $\mathbf{A}$ and $\mathbf{B}$ are isomorphic if there exists a permutation matrix $\mathbf{P}$ for which the identity $\mathbf{P}^{\mathrm{T}} \mathbf{A} \mathbf{P} = \mathbf{B}$ holds. Multiplying through by $\mathbf{P}$ and relaxing the permutation matrix to a doubly stochastic matrix leads to the linear programming relaxation known as fractional isomorphism. We show that the levels of the Sherali--Adams (SA) hierarchy of linear programming relaxations applied to fractional isomorphism interleave in power with the levels of a well-known color-refinement heuristic for graph isomorphism called the Weisfeiler--Lehman algorithm, or, equivalently, with the levels of indistinguishability in a logic with counting quantifiers and a bounded number of variables. This tight connection has quite striking consequences. For example, it follows immediately from a deep result of Grohe in the context of logics with counting quantifiers that a fixed number of levels of SA suffice to determine isomorphism of planar and minor-free graphs. We also offer applications in both finite model theory and polyhedral combinatorics. First, we show that certain properties of graphs, such as that of having a flow circulation of a prescribed value, are definable in the infinitary logic with counting with a bounded number of variables. Second, we exploit a lower bound construction due to Cai, Fürer, and Immerman in the context of counting logics to give simple explicit instances that show that the SA relaxations of the vertex-cover and cut polytopes do not reach their integer hulls for up to $\Omega(n)$ levels, where $n$ is the number of vertices in the graph.

Two graphs with adjacency matrices A and B are isomorphic if there exists a permutation matrix P for which the identity PTAP = B holds. Multiplying through by P and relaxing the permutation matrix to a doubly stochastic matrix leads to the linear programming relaxation known as fractional isomorphism. We show that the levels of the Sherali-Adams (SA) hierarchy of linear programming relaxations applied to fractional isomorphism interleave in power with the levels of a well-known color-refinement heuristic for graph isomorphism called the Weisfeiler-Lehman algorithm, or equivalently, with the levels of indistinguishability in a logic with counting quantifiers and a bounded number of variables. This tight connection has quite striking consequences. For example, it follows immediately from a deep result of Grohe in the context of logics with counting quantifiers, that a fixed number of levels of SA suffice to determine isomorphism of planar and minor-free graphs. We also offer applications both in finite model theory and polyhedral combinatorics. First, we show that certain properties of graphs, such as that of having a flow-circulation of a prescribed value, are definable in the infinitary logic with counting with a bounded number of variables. Second, we exploit a lower bound construction due to Cai, Fürer and Immerman in the context of counting logics to give simple explicit instances that show that the SA relaxations of the vertex-cover and cut polytopes do not reach their integer hulls for up to Ω(n) levels, where n is the number of vertices in the graph.

This note advertises the topics that will be covered in the tutorial on finite model theory.

We offer a new understanding of some aspects of practical SAT-solvers that are based on DPLL with unit-clause propagation, clause-learning, and restarts. We do so by analyzing a concrete algorithm which we claim is faithful to what practical solvers do. In particular, before making any new decision or restart, the solver repeatedly applies the unit-resolution rule until saturation, and leaves no component to the mercy of non-determinism except for some internal randomness. We prove the perhaps surprising fact that, although the solver is not explicitly designed for it, with high probability it ends up behaving as width-k resolution after no more than O(n^{2k+2}) conflicts and restarts, where n is the number of variables. In other words, width-k resolution can be thought of as O(n^{2k+2}) restarts of the unit-resolution rule with learning.

Relational joins are at the core of relational algebra, which in turn is the core of the standard database query language SQL. As their evaluation is expensive and very often dominated by the output size, it is an important task for database query optimisers to compute estimates on the size of joins and to find good execution plans for sequences of joins. We study these problems from a theoretical perspective, both in the worst-case model, and in an average-case model where the database is chosen according to a known probability distribution. In the former case, our first key observation is that the worst-case size of a query is characterised by the fractional edge cover number of its underlying hypergraph, a combinatorial parameter previously known to provide an upper bound. We complete the picture by proving a matching lower bound, and by showing that there exist queries for which the join-project plan suggested by the fractional edge cover approach may be substantially better than any join plan that does not use intermediate projections.

A class of relational structures is said to have the extension preservation property if every first-order sentence that is preserved under extensions on the class is equivalent to an existential sentence. The class of all finite structures does not have the extension preservation property. We study the property on classes of finite structures that are better behaved. We show that the property holds for classes of acyclic structures, structures of bounded degree, and more generally structures that are wide in a sense that we will make precise. We also show that the preservation property holds for the class of structures of treewidth at most k, for any k. In contrast, we show that the property fails for the class of planar graphs.

We may believe SAT does not have small Boolean circuits. But is it possible that some language with small circuits looks indistinguishable from SAT to every polynomial-time bounded adversary? We rule out this possibility. More precisely, assuming SAT does not have small circuits, we show that for every language A with small circuits, there exists a probabilistic polynomial-time algorithm that makes black-box queries to A, and produces, for a given input length, a Boolean formula on which A differs from SAT. A key step for obtaining this result is a new proof of the main result by Gutfreund, Shaltiel, and Ta-Shma reducing average-case hardness to worst-case hardness via uniform adversaries that know the algorithm they fool. The new adversary we construct has the feature of being black-box on the algorithm it fools, so it makes sense in the non-uniform setting as well. Our proof makes use of a refined analysis of the learning algorithm of Bshouty et al

Unions of conjunctive queries, also known as select-project-join-union queries, are the most frequently asked queries in relational database systems. These queries are definable by existential positive first-order formulas and are preserved under homomorphisms. A classical result of mathematical logic asserts that the existential positive formulas are the only first-order formulas (up to logical equivalence) that are preserved under homomorphisms on all structures, finite and infinite. The question of whether the homomorphism-preservation theorem holds for the class of all finite structures resisted solution for a long time. It was eventually shown that, unlike other classical preservation theorems, the homomorphism-preservation theorem does hold in the finite. In this article, we show that the homomorphism-preservation theorem holds also for several restricted classes of finite structures of interest in graph theory and database theory. Specifically, we show that this result holds for all classes of finite structures of bounded degree, all classes of finite structures of bounded treewidth, and, more generally, all classes of finite structures whose cores exclude at least one minor.

It is known that every constraint-satisfaction problem (CSP) reduces, and is in fact polynomially equivalent, to a digraph coloring problem. By carefully analyzing the constructions, we observe that the reduction is quantifierfree. Using this, we illustrate the power of the logical approach to CSPs by resolving two conjectures about treewidth duality in the digraph case. The point is that the analogues of these conjectures for general CSPs were resolved long ago by proof techniques that break down for digraphs. We also completely characterize those CSPs that are first-order definable and show that they coincide with those that have finitary tree duality. The combination of this result with an older result by Neˇsetˇril and Tardif shows that there is a computable listing of all template structures whose CSP is definable in full first-order logic. Finally, we provide new width lower bounds for some tractable CSPs. The novelty is that our bounds are a tight function of the treewidth of the underlying instance. As a corollary we get a new proof that there exist tractable CSPs without bounded treewidth duality. ∗ This work was partially supported by CICYT TIN2004-04343 and by the European Commision through the RTN COMBSTRU HPRN-CT2002-00278. 1 1

We consider the question of certifying unsatisfiability of random 3-CNF formulas. At which densities can we hope for a simple sufficient condition for unsatisfiability that holds almost surely? We study this question from the point of view of definability theory. The main result is that first-order logic cannot express any sufficient condition that holds almost surely on random 3-CNF formulas with n/sup 2-/spl alpha// clauses, for any irrational positive number /spl alpha/. In contrast, it can when the number of clauses is n/sup 2+/spl alpha//, for any positive /spl alpha/. As an intermediate step, our proof exploits the planted distribution for 3-CNF formulas in a new technical way. Moreover, the proof requires us to extend the methods of Shelah and Spencer for proving the zero-one law for sparse random graphs to arbitrary relational languages.

Unions of conjunctive queries, also known as select-project-join-union queries, are the most frequently asked queries in relational database systems. These queries are definable by existential positive first-order formulas and are preserved under homomorphisms. A classical result of mathematical logic asserts that existential positive formulas are the only first-order formulas (up to logical equivalence) that are preserved under homomorphisms on all structures, finite and infinite. It is long-standing open problem in finite model theory, however, to determine whether the same homomorphism-preservation result holds in the finite, that is, whether every first-order formula preserved under homomorphisms on finite structures is logically equivalent to an existential positive formula on finite structures. In this paper, we show that the homomorphism-preservation theorem holds for several large classes of finite structures of interest in graph theory and database theory. Specifically, we show that this result holds for all classes of finite structures of bounded degree, all classes of finite structures of bounded treewidth, and, more generally, all classes of finite structures whose cores exclude at least one minor.

A descriptive complexity approach to random 3-SAT is initiated. We show that unsatisfiability of any significant fraction of random 3-CNF formulas cannot be certified by any property that is expressible in Datalog. Combined with the known relationship between the complexity of constraint satisfaction problems and expressibility in Datalog, our result implies that any constraint propagation algorithm working with small constraints will fail to certify unsatisfiability almost always. Our result is a consequence of designing a winning strategy for one of the players in the existential pebble game. The winning strategy makes use of certain extension axioms that we introduce and hold almost surely on a random 3-CNF formula. The second contribution of our work is the connection between finite model theory and propositional proof complexity. To make this connection explicit, we establish a tight relationship between the number of pebbles needed to win the game and the width of the Resolution refutations. As a consequence to our result and the known size--width relationship in Resolution, we obtain new proofs of the exponential lower bounds for Resolution refutations of random 3-CNF formulas and the Pigeonhole Principle.

We prove that every property of 3CNF formulas that implies unsatisfiability and is expressible in Datalog has asymptotic probability zero when formulas are randomly generated by taking 6n non-trivial clauses of exactly three literals uniformly and independently. Our result is a consequence of designing a winning strategy for Duplicator in the existential k-pebble game on the structure that encodes the 3CNF formula and a fixed template structure encoding a satisfiable formula. The winning strategy makes use of certain extension axioms that we introduce and hold almost surely on a random 3CNF formula. An interesting feature of our result is that it brings the fields of propositional proof complexity and finite model theory together. To make this connection more explicit, we show that Duplicator wins the existential pebble game on the structure encoding the pigeonhole principle and the template structure above. Moreover, we also prove that there exists a 2k-Datalog program expressing that an input 3CNF formula has a resolution refutation of width k. As a consequence to our result and the known size-width relationship in resolution, we obtain new proofs of the exponential lower bounds for resolution refutations of random 3CNF formulas and the pigeonhole principle.

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.

The ordered conjecture states that least fixed-point logic LFP is strictly more expressive than first-order logic FO on every infinite class of ordered finite structures. It has been established that either way of settling this conjecture would resolve open problems in complexity theory. In fact, this holds true even for the particular instance of the ordered conjecture on the class of BIT-structures, that is, ordered finite structures with a built-in BIT predicate. Using a well known isomorphism from the natural numbers to the hereditarily finite sets that maps BIT to the membership relation between sets, the ordered conjecture on BIT-structures can be translated to the problem of comparing the expressive power of FO and LFP in the context of finite set theory. The advantage of this approach is that we can use set-theoretic concepts and methods to identify certain fragments of LFP for which the restriction of the ordered conjecture is already hard to settle, as well as other restricted fragments of LFP that actually collapse to FO. These results advance the state of knowledge about the ordered conjecture on BIT-structures and contribute to the delineation of the boundary where this conjecture becomes hard to settle.