Ruiwen Chen, Valentine Kabanets

We revisit the gate elimination method, generalize it to prove correlation bounds of boolean circuits with Parity, and also derive deterministic #SAT algorithms for small linear-size circuits. In particular, we prove that, for boolean circuits of size $3n - n^{0.51}$, the correlation with Parity is at most $2^{-n^{\Omega(1)}}$, and there ... more >>>

Ruiwen Chen

We give a \#SAT algorithm for boolean formulas over arbitrary finite bases. Let $B_k$ be the basis composed of all boolean functions on at most $k$ inputs. For $B_k$-formulas on $n$ inputs of size $cn$, our algorithm runs in time $2^{n(1-\delta_{c,k})}$ for $\delta_{c,k} = c^{-O(c^2k2^k)}$. We also show the average-case ... more >>>

Ruiwen Chen, Rahul Santhanam

We give improved deterministic algorithms solving sparse instances of MAX-SAT and MAX-$k$-CSP. For instances with $n$ variables and $cn$ clauses (constraints), we give algorithms running in time $\poly(n)\cdot 2^{n(1-\mu)}$ for

\begin{itemize}

\item $\mu = \Omega(\frac{1}{c} )$ and polynomial space solving MAX-SAT and MAX-$k$-SAT,

\item $\mu = \Omega(\frac{1}{\sqrt{c}} )$ and ...
more >>>

Dmitry Itsykson, Alexander Knop, Andrei Romashchenko, Dmitry Sokolov

In 2004 Atserias, Kolaitis and Vardi proposed OBDD-based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of identically false OBDD from OBDDs representing clauses of the initial formula. All OBDDs in such proofs have the same order of variables. We initiate the study of OBDD based ... more >>>