Nathan Segerlind

We demonstrate a family of propositional formulas in conjunctive normal form

so that a formula of size $N$ requires size $2^{\Omega(\sqrt[7]{N/logN})}$

to refute using the tree-like OBDD refutation system of

Atserias, Kolaitis and Vardi

with respect to all variable orderings.

All known symbolic quantifier elimination algorithms for satisfiability

generate ...
more >>>

Rahul Santhanam, Srikanth Srinivasan

Impagliazzo, Paturi and Zane (JCSS 2001) proved a sparsification lemma for $k$-CNFs:

every k-CNF is a sub-exponential size disjunction of $k$-CNFs with a linear

number of clauses. This lemma has subsequently played a key role in the study

of the exact complexity of the satisfiability problem. A natural question is

more >>>

Rahul Santhanam

I discuss recent progress in developing and exploiting connections between

SAT algorithms and circuit lower bounds. The centrepiece of the article is

Williams' proof that $NEXP \not \subseteq ACC^0$, which proceeds via a new

algorithm for $ACC^0$-SAT beating brute-force search. His result exploits

a formal connection from non-trivial SAT algorithms ...
more >>>

Rahul Santhanam, Ryan Williams

We revisit the complexity of the satisfiability problem for quantified Boolean formulas. We show that satisfiability

of quantified CNFs of size $\poly(n)$ on $n$ variables with $O(1)$

quantifier blocks can be solved in time $2^{n-n^{\Omega(1)}}$ by zero-error

randomized algorithms. This is the first known improvement over brute force search in ...
more >>>

Ruiwen Chen, Rahul Santhanam, Srikanth Srinivasan

We show average-case lower bounds for explicit Boolean functions against bounded-depth threshold circuits with a superlinear number of wires. We show that for each integer d > 1, there is \epsilon_d > 0 such that Parity has correlation at most 1/n^{\Omega(1)} with depth-d threshold circuits which have at most

n^{1+\epsilon_d} ...
more >>>

Igor Carboni Oliveira, Ruiwen Chen, Rahul Santhanam

In a seminal work, Williams [Wil14] showed that NEXP (non-deterministic exponential time) does not have polynomial-size ACC^0 circuits. Williams' technique inherently gives a worst-case lower bound, and until now, no average-case version of his result was known.

We show that there is a language L in NEXP (resp. EXP^NP) ... more >>>