Related papers: Resolution and the binary encoding of combinatoria…
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 consider Proof Complexity in light of the unusual binary encoding of certain combinatorial principles. We contrast this Proof Complexity with the normal unary encoding in several refutation systems, based on Resolution and Integer Linear…
We provide a number of simplified and improved separations between pairs of Resolution-with-bounded-conjunction refutation systems, Res(d), as well as their tree-like versions, Res*(d). The contradictions we use are natural combinatorial…
In this paper we study an extension of the Polynomial Calculus proof system where we can introduce new variables and take a square root. We prove that an instance of the subset-sum principle, the binary value principle, requires refutations…
Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted Res(lin_R), this refutation system operates with disjunctions of linear…
In this paper we prove lower bounds for sizes of refutations of unsatisfiable vector Subset Sum instances $\overrightarrow{a}_1 x_1 + \dots + \overrightarrow{a}_n x_n = \overrightarrow{b}$ in the proof system Res(lin$_{\mathbb{F}_q}$) where…
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)…
We consider the Sherali-Adams (SA) refutation system together with the unusual binary encoding of certain combinatorial principles. For the unary encoding of the Pigeonhole Principle and the Least Number Principle, it is known that linear…
We present a Rice-like complexity lower bound for any MSO-definable problem on binary structures succinctly encoded by circuits. This work extends the framework recently developed as a counterpoint to Courcelle's theorem for graphs encoded…
We prove superpolynomial length lower bounds for the semantic tree-like Frege refutation system with bounded line size. Concretely, for any function $n^{2-\varepsilon} \leq s(n) \leq 2^{n^{1-\varepsilon}}$ we exhibit an explicit family…
A binary code Enc$:\{0,1\}^k \to \{0,1\}^n$ is $(0.5-\epsilon,L)$-list decodable if for all $w \in \{0,1\}^n$, the set List$(w)$ of all messages $m \in \{0,1\}^k$ such that the relative Hamming distance between Enc$(m)$ and $w$ is at most…
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…
Folded Reed-Solomon (FRS) and univariate multiplicity codes are prominent polynomial codes over finite fields, renowned for achieving list decoding capacity. These codes have found a wide range of applications beyond the traditional scope…
Motivated by an application where we try to make proofs for Description Logic inferences smaller by rewriting, we consider the following decision problem, which we call the small term reachability problem: given a term rewriting system $R$,…
Proving proof-size lower bounds for $\mathbf{LK}$, the sequent calculus for classical propositional logic, remains a major open problem in proof complexity. We shed new light on this challenge by isolating the power of structural rules,…
We investigate the space complexity of refuting $3$-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random $3$-CNF $\phi$ in $n$ variables requires, with high probability,…
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 prove lower bounds for proofs of the bit pigeonhole principle (BPHP) and its generalizations in bounded-depth resolution over parities (Res$(\oplus)$). For weak BPHP$_n^m$ with $m = cn$ pigeons (for any constant $c>1$) and $n$ holes, for…
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…
The reflection principle is the statement that if a sentence is provable then it is true. Reflection principles have been studied for first-order theories, but they also play an important role in propositional proof complexity. In this…