Related papers: Space proof complexity for random 3-CNFs

We investigate the space complexity of refuting $3$-CNFs in Resolution and algebraic systems. No lower bound for refuting any family of $3$-CNFs was previously known for the total space in resolution or for the monomial space in algebraic…

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 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…

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 study -- within the framework of propositional proof complexity -- the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiable formula has many satisfying assignments, where ``many'' stands for an…

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…

Let $\phi$ be a 3CNF formula with n variables and m clauses. A simple nonconstructive argument shows that when m is sufficiently large compared to n, most 3CNF formulas are not satisfiable. It is an open question whether there is an…

Let $P:\{0,1\}^k \to \{0,1\}$ be a nontrivial $k$-ary predicate. Consider a random instance of the constraint satisfaction problem $\mathrm{CSP}(P)$ on $n$ variables with $\Delta n$ constraints, each being $P$ applied to $k$ randomly chosen…

Atserias and M\"uller (JACM, 2020) proved that for every unsatisfiable CNF formula $\varphi$, the formula $\operatorname{Ref}(\varphi)$, stating "$\varphi$ has small Resolution refutations", does not have subexponential-size Resolution…

In this paper, we analyze 2CNF formulas from the perspectives of Read-Once resolution (ROR) refutation schemes. We focus on two types of ROR refutations, viz., variable-once refutation and clause-once refutation. In the former, each…

We study the *refuter* problems for proof complexity lower bounds. Suppose $\varphi$ is a hard tautology that does not admit any length-$s$ proof in some proof system $P$. In the corresponding refuter problem, we are given (query access to)…

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 investigate the size complexity of proofs in $Res(s)$ -- an extension of Resolution working on $s$-DNFs instead of clauses -- for families of contradictions given in the {\em unusual binary} encoding. A motivation of our work is size…

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…

This work studies the complexity of refuting the existence of a perfect matching in spectral expanders with an odd number of vertices, in the Polynomial Calculus (PC) and Sum of Squares (SoS) proof system. Austrin and Risse [SODA, 2021]…

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…

We analyse how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, and semi-algebraic proof systems, the classical constructions of…

We consider the average-case complexity of some otherwise undecidable or open Diophantine problems. More precisely, consider the following: (I) Given a polynomial f in Z[v,x,y], decide the sentence \exists v \forall x \exists y f(v,x,y)=0,…

For every $n >0$, we show the existence of a CNF tautology over $O(n^2)$ variables of width $O(\log n)$ such that it has a Polynomial Calculus Resolution refutation over $\{0,1\}$ variables of size $O(n^3polylog(n))$ but any Polynomial…

We present a general method for converting any family of unsatisfiable CNF formulas that is hard for one of the simplest proof systems, tree resolution, into formulas that require large rank in any proof system that manipulates polynomials…