We show that tree-like OBDD proofs of unsatisfiability require an exponential increase ($s \mapsto 2^{s^{\Omega(1)}}$) in proof size to simulate unrestricted resolution, and that unrestricted OBDD proofs of unsatisfiability require an almost-exponential increase ($s \mapsto 2^{ 2^{\left( \log s \right)^{\Omega(1)}}}$) in proof size to simulate $\Res{O(\log n)}$. The ``OBDD proof ... more >>>

For any given Boolean formula $\phi(x_1,\dots,x_n)$, one can
efficiently construct (using \emph{arithmetization}) a low-degree
polynomial $p(x_1,\dots,x_n)$ that agrees with $\phi$ over all
points in the Boolean cube $\{0,1\}^n$; the constructed polynomial
$p$ can be interpreted as a polynomial over an arbitrary field
$\mathbb{F}$. The problem ... more >>>

In this paper we give the first deterministic polynomial time algorithm for testing whether a {\em diagonal} depth-$3$ circuit $C(\arg{x}{n})$ (i.e. $C$ is a sum of powers of linear functions) is zero. We also prove an exponential lower bound showing that such a circuit will compute determinant or permanent only ... more >>>