Michael Alekhnovich, Eli Ben-Sasson

We analyze the efficiency of the random walk algorithm on random 3CNF instances, and prove em linear upper bounds on the running time

of this algorithm for small clause density, less than 1.63. Our upper bound matches the observed running time to within a multiplicative factor. This is the ...
more >>>

Eran Ofek, Uriel Feige

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 efficient

refutation algorithm that for most such formulas proves ...
more >>>

Iddo Tzameret

We formalize a combinatorial principle, called the 3XOR principle, due to Feige, Kim and Ofek (2006), as a family of unsatisfiable propositional formulas for which refutations of small size in any propositional proof system that possesses the feasible interpolation property imply an efficient *deterministic* refutation algorithm for random 3SAT with ... more >>>