Related papers: Supercritical Space-Width Trade-offs for Resolutio…
In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of CNF formulas is always an upper bound on the width needed to refute them. Their proof is beautiful…
For current state-of-the-art DPLL SAT-solvers the two main bottlenecks are the amounts of time and memory used. In proof complexity, these resources correspond to the length and space of resolution proofs. There has been a long line of…
For any unsatisfiable CNF formula we give an exponential lower bound on the size of resolution refutations of a propositional statement that the formula has a resolution refutation. We describe three applications. (1) An open question in…
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^Omega(w). This shows that the simple counting argument that any formula refutable in width w must…
In the context of proving lower bounds on proof space in k-DNF resolution, [Ben-Sasson and Nordstrom 2009] introduced the concept of minimally unsatisfiable sets of k-DNF formulas and proved that a minimally unsatisfiable k-DNF set with m…
We exhibit a monotone function computable by a monotone circuit of quasipolynomial size such that any monotone circuit of polynomial depth requires exponential size. This is the first size-depth tradeoff result for monotone circuits in the…
We exhibit supercritical trade-off for monotone circuits, showing that there are functions computable by small circuits for which any circuit must have depth super-linear or even super-polynomial in the number of variables, far exceeding…
We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Tor\'an and W\"orz (TOCL 2023) showed that there is a resolution refutation of narrow width $k$ for two graphs if and only if they can be…
Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The main bottleneck for such algorithms, other than the obvious one of time, is the amount of memory used. In the field…
We study the complexity of the following "resolution width problem": Does a given 3-CNF have a resolution refutation of width k? We prove that the problem cannot be decided in time O(n^((k-3)/12)). This lower bound is unconditional and does…
A major open problem in proof complexity is to demonstrate that random 3-CNFs with a linear number of clauses require super-polynomial size refutations in bounded-depth Frege systems. We take the first step towards addressing this question…
We show tight lower bounds for the entire trade-off between space and query time for the Approximate Near Neighbor search problem. Our lower bounds hold in a restricted model of computation, which captures all hashing-based approaches. In…
We investigate the `local consistency implies global consistency' principle of strict width among structures within the scope of the Bodirsky-Pinsker dichotomy conjecture for infinite-domain Constraint Satisfaction Problems (CSPs). Our main…
Hardness magnification reduces major complexity separations (such as $\mathsf{\mathsf{EXP}} \nsubseteq \mathsf{NC}^1$) to proving lower bounds for some natural problem $Q$ against weak circuit models. Several recent works [OS18, MMW19,…
The path to the solution of Feder-Vardi dichotomy conjecture by Bulatov and Zhuk led through showing that more and more general algebraic conditions imply polynomial-time algorithms for the finite-domain Constraint Satisfaction Problems…
Two major considerations when encoding pseudo-Boolean (PB) constraints into SAT are the size of the encoding and its propagation strength, that is, the guarantee that it has a good behaviour under unit propagation. Several encodings with…
In this paper we establish an improved outer bound on the storage-repair-bandwidth tradeoff of regenerating codes under exact repair. The result shows that in particular, it is not possible to construct exact-repair regenerating codes that…
We show that bounded self-contracted curves are rectifiable in metric spaces with weak lower curvature bound in a sense we introduce in this article. This class of spaces is wide and includes, for example, finite-dimensional Alexandrov…
This paper considers the length of resolution proofs when using Krishnamurthy's classic symmetry rules. We show that inconsistent linear equation systems of bounded width over a fixed finite field $\mathbb{F}_p$ with $p$ a prime have, in…
The last decade has seen a revival of interest in pebble games in the context of proof complexity. Pebbling has proven a useful tool for studying resolution-based proof systems when comparing the strength of different subsystems, showing…