Time-bounded conditional Kolmogorov complexity of a string x given y, Kt(x∣ y), is the length of a shortest program that, given y, prints x within t steps. The Chain Rule for conditional Kt with error e is the following hypothesis: there is a constant c such that, for any strings y,x1,…,xℓ∈{0,1}*, for any ℓ∈ℕ, and all sufficiently large time bounds t,

In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. However, previous work does not address the tightness of the simulation, i.e., the question of how large this overhead needs to be. In this paper, we address this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning schemes, namely that the derivation of a learned clause has at least one inference where a literal appears in both premises (aka, a merge literal). Specifically, we show that proofs of this kind can simulate resolution proofs with at most a linear overhead, but there also exist formulas where such overhead is necessary or, more precisely, that there exist formulas with resolution proofs of linear length that require quadratic CDCL proofs.

We generalize the ``indirect learning'' technique of Furst et al. (1991) to reduce from learning a concept class over a samplable distribution $\mu$ to learning the same concept class over the uniform distribution. The reduction succeeds when the sampler for $\mu$ is both contained in the target concept class and efficiently invertible in the sense of Impagliazzo and Luby (1989). We give two applications. We show that $\mathsf{AC}^0[q]$ is learnable over any succinctly-described product distribution. $\mathsf{AC}^0[q]$ is the class of constant-depth Boolean circuits of polynomial size with AND, OR, NOT, and counting modulo $q$ gates of unbounded fanins. Our algorithm runs in randomized quasi-polynomial time and uses membership queries. If there is a strongly useful natural property in the sense of Razborov and Rudich (1997) — an efficient algorithm that can distinguish between random strings and strings of non-trivial circuit complexity — then general polynomial-sized Boolean circuits are learnable over any efficiently samplable distribution in randomized polynomial time, given membership queries to the target function.

We investigate randomized LEARN-uniformity, which captures the power of randomness and equivalence queries (EQ) in the construction of Boolean circuits for an explicit problem. This is an intermediate notion between P-uniformity and non-uniformity motivated by connections to learning, complexity, and logic. Building on a number of techniques, we establish the first unconditional lower bounds against LEARN-uniform circuits: –For all$c\geq 1$, there is$L\in \mathsf{P}$that is not computable by circuits of size$n\cdot(\log n)^{c}$generated in deterministic polynomial time with$o(\log n/\log\log n)$equivalence queries to$L$. In other words, small circuits for$L$cannot be efficiently learned using a bounded number of EQs. –For each$k\geq 1$, there is$L\in \mathsf{NP}$such that circuits for$L$of size$O(n^{k})$cannot be learned in deterministic polynomial time with access to$n^{o(1)}$EQs. –For each$k\geq 1$, there is a problem in promise-ZPP that is not in FZPP-uniform$\mathsf{SIZE}[n^{k}]$. –Conditional and unconditional lower bounds against LEARN-uniform circuits in the general setting with randomized uniformity and access to EQs. In all these lower bounds, the learning algorithm may run in arbitrary polynomial time, while the hard problem is computed in some fixed polynomial time. We employ these results to investigate the (un)provability of non-uniform circuit upper bounds (e.g., Is N P contained in$\mathsf{SIZE}[n^{3}]?)$in theories of bounded arithmetic. Some questions of this form have been addressed in recent papers of Krajíček-Oliveira (2017), Müller-Bydzovsky (2020), and Bydzovsky-Krajíček-Oliveira (2020) via a mixture of techniques from proof theory, complexity theory, and model theory. In contrast, by extracting computational information from proofs via a direct translation to LEARN-uniformity, we establish robust unprovability theorems that unify, simplify, and extend nearly all previous results. In addition, our lower bounds against randomized LEARN-uniformity yield unprovability results for theories augmented with the dual weak pigeonhole principle, such as APC1(Jeřábek, 2007), which is known to formalize a large fragment of modern complexity theory. Finally, we make precise potential limitations of theories of bounded arithmetic such as PV (Cook, 1975) and Jeřábek's theory APC1, by showing unconditionally that these theories cannot prove statements like “$\mathsf{NP}\not\subseteq \mathsf{BPP}\wedge \mathsf{NP}\subset \mathsf{io}-\mathsf{P}/\mathsf{poly}$”, i.e., that N P is uniformly “hard” but non-uniformly “easy” on infinitely many input lengths. In other words, if we live in such a complexity world, then this cannot be established feasibly.

Lifting arguments show that the complexity of a function in one model is essentially that of a related function (often the composition of the original function with a small function called a gadget) in a more powerful model. Lifting has been used to prove strong lower bounds in communication complexity, proof complexity, circuit complexity and many other areas. We present a lifting construction for constant depth unbounded fan-in circuits. Given a function f, we construct a function g, so that the depth d+1 circuit complexity of g, with a certain restriction on bottom fan-in, is controlled by the depth d circuit complexity of f, with the same restriction. The function g is defined as f composed with a parity function. With some quantitative losses, average-case and general depth-d circuit complexity can be reduced to circuit complexity with this bottom fan-in restriction. As a consequence, an algorithm to approximate the depth d (for any d > 3) circuit complexity of given (truth tables of) Boolean functions yields an algorithm for approximating the depth 3 circuit complexity of functions, i.e., there are quasi-polynomial time mapping reductions between various gap-versions of AC⁰-MCSP. Our lifting results rely on a blockwise switching lemma that may be of independent interest. We also show some barriers on improving the efficiency of our reductions: such improvements would yield either surprisingly efficient algorithms for MCSP or stronger than known AC⁰ circuit lower bounds.

We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [44], and show that this analysis can be formalized in the bounded arithmetic system VNC1 (corresponding to the “NC1 reasoning”). As a corollary, we prove the assumption made by Jeřábek [28] that a construction of certain bipartite expander graphs can be formalized in VNC1. This in turn implies that every proof in Gentzen's sequent calculus LK of a monotone sequent can be simulated in the monotone version of LK (MLK) with only polynomial blowup in proof size, strengthening the quasipolynomial simulation result of Atserias, Galesi, and Pudlák [9].

Minimum Circuit Size Problem (MCSP) asks to decide if a given truth table of an n-variate boolean function has circuit complexity less than a given parameter s. We prove that MCSP is hard for constant-depth circuits with mod p gates, for any prime p >= 2 (the circuit class AC^0[p]). Namely, we show that MCSP requires d-depth AC^0[p] circuits of size at least exp(N^{0.49/d}), where N=2^n is the size of an input truth table of an n-variate boolean function. Our circuit lower bound proof shows that MCSP can solve the coin problem: distinguish uniformly random N-bit strings from those generated using independent samples from a biased random coin which is 1 with probability 1/2+N^{-0.49}, and 0 otherwise. Solving the coin problem with such parameters is known to require exponentially large AC^0[p] circuits. Moreover, this also implies that MAJORITY is computable by a non-uniform AC^0 circuit of polynomial size that also has MCSP-oracle gates. The latter has a few other consequences for the complexity of MCSP, e.g., we get that any boolean function in NC^1 (i.e., computable by a polynomial-size formula) can also be computed by a non-uniform polynomial-size AC^0 circuit with MCSP-oracle gates.

Properties definable in first-order logic are algorithmically interesting for both theoretical and pragmatic reasons. Many of the most studied algorithmic problems, such as Hitting Set and Orthogonal Vectors, are first-order, and the first-order properties naturally arise as relational database queries. A relatively straightforward algorithm for evaluating a property with k +1 quantifiers takes time O ( m k ) and, assuming the Strong Exponential Time Hypothesis (SETH), some such properties require O ( m k −ϵ) time for any ϵ > 0. (Here, > m represents the size of the input structure, i.e., the number of tuples in all relations.) We give algorithms for every first-order property that improves this upper bound to m k /2 Θ (√ log n ) , i.e., an improvement by a factor more than any poly-log, but less than the polynomial required to refute SETH. Moreover, we show that further improvement is equivalent to improving algorithms for sparse instances of the well-studied Orthogonal Vectors problem. Surprisingly, both results are obtained by showing completeness of the Sparse Orthogonal Vectors problem for the class of first-order properties under fine-grained reductions. To obtain improved algorithms, we apply the fast Orthogonal Vectors algorithm of References [3, 16]. While fine-grained reductions (reductions that closely preserve the conjectured complexities of problems) have been used to relate the hardness of disparate specific problems both within P and beyond, this is the first such completeness result for a standard complexity class.

The resolution proof system has been enormously helpful in deepening our understanding of conflict-driven clause-learning ( $$\mathsf {CDCL}$$ ) SAT solvers. In the interest of providing a similar proof complexity-theoretic analysis of satisfiability modulo theories (SMT) solvers, we introduce a generalization of resolution called Res(T). We show that many of the known results comparing resolution and $$\mathsf {CDCL}$$ solvers lift to the SMT setting, such as the result of Pipatsrisawat and Darwiche showing that $$\mathsf {CDCL}$$ solvers with “perfect” non-deterministic branching and an asserting clause-learning scheme can polynomially simulate general resolution. We also describe a stronger version of Res(T), $$\mathsf {Res}^*$$ (T), capturing SMT solvers allowing introduction of new literals. We analyze the theory EUF of equality with uninterpreted functions, and show that the $$\mathsf {Res}^*(\mathrm {EUF})$$ system is able to simulate an earlier calculus introduced by Bjørner and de Moura for the purpose of analyzing $$\mathsf {DPLL}$$ (EUF). Further, we show that $$\mathsf {Res}^*(\mathrm {EUF})$$ (and thus SMT algorithms with clause learning over EUF, new literal introduction rules and perfect branching) can simulate the Frege proof system, which is well-known to be far more powerful than resolution. Finally, we prove under the Exponential Time Hypothesis (ETH) that any reduction from EUF to SAT (such as the Ackermann reduction) must, in the worst case, produce an instance of size $$\varOmega (n \log n)$$ from an instance of size n.

We introduce and develop a new semi-algebraic proof system, called Stabbing Planes that is in the style of DPLL-based modern SAT solvers. As with DPLL, there is only one rule: the current polytope can be subdivided by branching on an inequality and its "integer negation." That is, we can (nondeterministically choose) a hyperplane a x >= b with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying a x >= b, the points satisfying a x <= b-1, and the middle slab b-1 < a x < b. Since the middle slab contains no integer points it can be safely discarded, and the algorithm proceeds recursively on the other two branches. Each path terminates when the current polytope is empty, which is polynomial-time checkable. Among our results, we show somewhat surprisingly that Stabbing Planes can efficiently simulate Cutting Planes, and moreover, is strictly stronger than Cutting Planes under a reasonable conjecture. We prove linear lower bounds on the rank of Stabbing Planes refutations, by adapting a lifting argument in communication complexity.

We generalize the "learning algorithms from natural properties" framework of [CIKK16] to get agnostic learning algorithms from natural properties with extra features. We show that if a natural property (in the sense of Razborov and Rudich [RR97]) is useful also against functions that are close to the class of "easy" functions, rather than just against "easy" functions, then it can be used to get an agnostic learning algorithm over the uniform distribution with membership queries. * For AC0[q], any prime q (constant-depth circuits of polynomial size, with AND, OR, NOT, and MODq gates of unbounded fanin), which happens to have a natural property with the requisite extra feature by [Raz87, Smo87, RR97], we obtain the first agnostic learning algorithm for AC0[q], for every prime q. Our algorithm runs in randomized quasi-polynomial time, uses membership queries, and outputs a circuit for a given Boolean function f that agrees with f on all but at most polylog(n)*opt fraction of inputs, where opt is the relative distance between f and the closest function h in the class AC0[q]. * For the ideal case, a natural proof of strongly exponential correlation circuit lower bounds against a circuit class C containing AC0[2] (i.e., circuits of size exp(Omega(n)) cannot compute some n-variate function even with exp(-Omega(n)) advantage over random guessing) would yield a polynomial-time query agnostic learning algorithm for C with the approximation error O(opt).

The Black-Box Hypothesisstates that any property of Boolean functions decided efficiently (e.g., in BPP) with inputs represented by circuits can also be decided efficiently in the black-box setting, where an algorithm is given an oracle access to the input function and an upper bound on its circuit size. If this hypothesis is true, then P neq NP. We focus on the consequences of the hypothesis being false, showing that (under general conditions on the structure of a counterexample) it implies a non-trivial algorithm for CSAT. More specifically, we show that if there is a property F of boolean functions such that F has high sensitivity on some input function f of subexponential circuit complexity (which is a sufficient condition for F being a counterexample to the Black-Box Hypothesis), then CSAT is solvable by a subexponential-size circuit family. Moreover, if such a counterexample F is symmetric, then CSAT is in Ppoly. These results provide some evidence towards the conjecture (made in this paper) that the Black-Box Hypothesis is false if and only if CSAT is easy.

Properties definable in first-order logic are algorithmically interesting for both theoretical and pragmatic reasons. Many of the most studied algorithmic problems, such as Hitting Set and Orthogonal Vectors, are first-order, and the first-order properties naturally arise as relational database queries. A relatively straightforward algorithm for evaluating a property with k + 1 quantifiers takes time O(mk) and, assuming the Strong Exponential Time Hypothesis (SETH), some such properties require O(mk-∊) time for any ∊ > 0. (Here, m represents the size of the input structure, i.e. the number of tuples in all relations.) We give algorithms for every first-order property that improves this upper bound to i.e., an improvement by a factor more than any poly-log, but less than the polynomial required to refute SETH. Moreover, we show that further improvement is equivalent to improving algorithms for sparse instances of the well-studied Orthogonal Vectors problem. Surprisingly, both results are obtained by showing completeness of the Sparse Orthogonal Vectors problem for the class of first-order properties under fine-grained reductions. To obtain improved algorithms, we apply the fast Orthogonal Vectors algorithm of [3, 16]. While fine-grained reductions (reductions that closely preserve the conjectured complexities of problems) have been used to relate the hardness of disparate specific problems both within P and beyond, this is the first such completeness result for a standard complexity class.

Based on Hastad's (1986) circuit lower bounds, Linial, Mansour, and Nisan (1993) gave a quasipolytime learning algorithm for AC^0 (constant-depth circuits with AND, OR, and NOT gates), in the PAC model over the uniform distribution. It was an open question to get a learning algorithm (of any kind) for the class of AC^0[p] circuits (constant-depth, with AND, OR, NOT, and MOD_p gates for a prime p). Our main result is a quasipolytime learning algorithm for AC^0[p] in the PAC model over the uniform distribution with membership queries. This algorithm is an application of a general connection we show to hold between natural proofs (in the sense of Razborov and Rudich (1997)) and learning algorithms. We argue that a natural proof of a circuit lower bound against any (sufficiently powerful) circuit class yields a learning algorithm for the same circuit class. As the lower bounds against AC^0[p] by Razborov (1987) and Smolensky (1987) are natural, we obtain our learning algorithm for AC^0[p].

We tighten the connections between circuit lower bounds and derandomization for each of the following three types of derandomization: - general derandomization of promiseBPP (connected to Boolean circuits), - derandomization of Polynomial Identity Testing (PIT) over fixed finite fields (connected to arithmetic circuit lower bounds over the same field), and - derandomization of PIT over the integers (connected to arithmetic circuit lower bounds over the integers). We show how to make these connections uniform equivalences, although at the expense of using somewhat less common versions of complexity classes and for a less studied notion of inclusion. Our main results are as follows: 1. We give the first proof that a non-trivial (nondeterministic subexponential-time) algorithm for PIT over a fixed finite field yields arithmetic circuit lower bounds. 2. We get a similar result for the case of PIT over the integers, strengthening a result of Jansen and Santhanam [JS12] (by removing the need for advice). 3. We derive a Boolean circuit lower bound for NEXP intersect coNEXP from the assumption of sufficiently strong non-deterministic derandomization of promiseBPP (without advice), as well as from the assumed existence of an NP-computable non-empty property of Boolean functions useful for proving superpolynomial circuit lower bounds (in the sense of natural proofs of [RR97]); this strengthens the related results of [IKW02]. 4. Finally, we turn all of these implications into equivalences for appropriately defined promise classes and for a notion of robust inclusion/separation (inspired by [FS11]) that lies between the classical "almost everywhere" and "infinitely often" notions.

We show that circuit lower bound proofs based on the method of random restrictions yield non-trivial compression algorithms for “easy” Boolean functions from the corresponding circuit classes. The compression problem is defined as follows: given the truth table of an n-variate Boolean function f computable by some unknown small circuit from a known class of circuits, find in deterministic time poly(2n) a circuit C (no restriction on the type of C) computing f so that the size of C is less than the trivial circuit size 2n/n. We get nontrivial compression for functions computable by AC0circuits, (de Morgan) formulas, and (read-once) branching programs of the size for which the lower bounds for the corresponding circuit class are known. These compression algorithms rely on the structural characterizations of “easy” functions, which are useful both for proving circuit lower bounds and for designing “meta-algorithms” (such as Circuit-SAT). For (de Morgan) formulas, such structural characterization is provided by the “shrinkage under random restrictions” results [52], [21], strengthened to the “high-probability” version by [48], [26], [33]. We give a new, simple proof of the “high-probability” version of the shrinkage result for (de Morgan) formulas, with improved parameters. We use this shrinkage result to get both compression and #SAT algorithms for (de Morgan) formulas of size about n2. We also use this shrinkage result to get an alternative proof of the recent result by Komargodski and Raz [33] of the average-case lower bound against small (de Morgan) formulas. Finally, we show that the existence of any non-trivial compression algorithm for a circuit class C ⊆ P/poly would imply the circuit lower bound NEXP ⊈ C. This complements Williams's result [55] that any non-trivial Circuit-SAT algorithm for a circuit class C would imply a superpolynomial lower bound against C for a language in NEXP1.

Complexity in logic comes in many forms. In finite model theory, it is the complexity of describing properties, whereas in proof complexity it is the complexity of proving properties in a proof system. Here, we consider several notions of complexity in logic, the connections among them and their relationship with computational complexity. In particular, we show how the complexity of logics in the setting of finite model theory is used to obtain results in bounded arithmetic, stating which functions are provably total in certain weak systems of arithmetic. For example, the transitive closure function (testing reachability between two given points in a directed graph) is definable using only NL-concepts (where NL is the non-deterministic logspace complexity class) and its totality (and, thus, the closure of NL under complementation) is provable within NL-reasoning. Lastly, we will touch upon the topic of formalizing complexity theory using logic, and the meta-question of complexity of logical reasoning about complexity-theoretic statements. This is intended to be a high-level overview, suitable for readers who are not familiar with complexity theory and complexity in logic.

Non-relativization of complexity issues can be interpreted as giving some evidence that these issues cannot be resolved by "black-box" techniques. In the early 1990's, a sequence of important non-relativizing results was proved, mainly using algebraic techniques. Two approaches have been proposed to understand the power and limitations of these algebraic techniques: (1) Fortnow [For94] gives a construction of a class of oracles which have a similar algebraic and logical structure, although they are arbitrarily powerful. He shows that many of the non-relativizing results proved using algebraic techniques hold for all such oracles, but he does not show, e.g., that the outcome of the "P vs. NP" question differs between different oracles in that class. (2) Aaronson and Wigderson [AW08] give definitions of algebrizing separations and collapses of complexity classes, by comparing classes relative to one oracle to classes relative to an algebraic extension of that oracle. Using these definitions, they show both that the standard collapses and separations "algebrize" and that many of the open questions in complexity fail to "algebrize", suggesting that the arithmetization technique is close to its limits. However, it is unclear how to formalize algebrization of more complicated complexity statements than collapses or separations, and whether the algebrizing statements are, e.g., closed under modus ponens so it is conceivable that several algebrizing premises could imply (in a relativizing way) a non-algebrizing conclusion. In this paper, building on the work of Arora, Impagliazzo, and Vazirani [AIV92], we propose an axiomatic approach to "algebrization", which complements and clarifies the approaches of [For94] and [AW08]. We present logical theories formalizing the notion of algebrizing techniques in the following sense: most known complexity results proved using arithmetization are provable within our theories, while many open questions are independent of the theories. So provability in the proposed theories can serve as a surrogate for provability using the arithmetization technique. Our theories extend the [AIV92] theory with a new axiom, Arithmetic Checkability which intuitively says that all NP languages have verifiers that are efficiently computable low-degree polynomials (over the integers). We show the following: (i) Arithmetic checkability holds relative to arbitrarily powerful oracles (since Fortnow's algebraic oracles from [For94] all satisfy the Arithmetic Checkability axiom). (ii) Most of the algebrizing collapses and separations from [AW08], such as IP=PSPACE, NP ⊂ ZKIP if one-way functions exist, MA-EXP ⊄ P poly, etc., are provable from Arithmetic Checkability.(iii) Many of the open complexity questions (including most of those shown to require non-algebrizing techniques in [AW08]), such as "P vs. NP", "NP vs. BPP", etc., cannot be proved from Arithmetic Checkability. (iv) Arithmetic Checkability is also insufficient to prove one known result, NEXP=MIP (although relative to an oracle satisfying Arithmetic Checkability, NEXPO restricted to poly-length queries is contained in MIPO, mirroring a similar result from [AW08]).

We introduce a second-order theory V-Krom of bounded arithmetic for nondeterministic log space. This system is based on Gradel's characterization of NL by second-order Krom formulae with only universal first-order quantifiers, which in turn is motivated by the result that the decision problem for 2-CNF satisfiability is complete for coNL (and hence for NL). This theory has the style of the authors' theory Vi-Horn [APAL 124 (2003)] for polynomial time. Both theories use Zambella's elegant second-order syntax, and are axiomatized by a set 2-BASIC of simple formulae, together with a comprehension scheme for either second-order Horn formulae (in the case of V/sub 1/-Horn), or second-order Krom (2CNF) formulae (in the case of V-Krom). Our main result for V-Krom is a formalization of the Immerman-Szelepcsenyi theorem that NL is closed under complementation. This formalization is necessary to show that the NL functions are /spl Sigma//sub 1//sup B/-definable in V-Krom. The only other theory for NL in the literature relies on the Immerman-Szelepcsenyi's result rather than proving it.

We introduce a second-order system V/sub 1/-Horn of bounded arithmetic formalizing polynomial-time reasoning, based on Gradel's (1992) second-order Horn characterization of P. Our system has comprehension over P predicates (defined by Gradel's second-order Horn formulas), and only finitely, many function symbols. Other systems of polynomial-time reasoning either allow induction on NP predicates (such as Buss's (1986) S/sub 2//sup 1/ or the second-order V/sub 1//sup 1/), and hence are more powerful than our system (assuming the polynomial hierarchy does not collapse), or use Cobham's theorem to introduce function symbols for all polynomial-time functions (such as Cook's PV and Zambella's P-def). We prove that our system is equivalent to QPV and Zambella's (1996) P-def. Using our techniques, we also show that V/sub 1/-Horn is finitely, axiomatizable, and, as a corollary, that the class of /spl forall//spl Sigma//sub 1//sup b/ consequences of S/sub 2//sup 1/ is finitely axiomatizable as well, thus answering an open question.