We give a deterministic algorithm for testing satisfiability of formulas in conjunctive normal form with no restriction on clause length. Its upper bound on the worst-case running time matches the best known upper bound for randomized satisfiability-testing algorithms [Dantsin and Wolpert, SAT 2005]. In comparison with the randomized algorithm in ... more >>>

We give a randomized algorithm for testing satisfiability of Boolean formulas in conjunctive normal form with no restriction on clause length. Its running time is at most $2^{n(1-1/\alpha)}$ up to a polynomial factor, where $\alpha = \ln(m/n) + O(\ln \ln m)$ and $n$, $m$ are respectively the number of variables ... more >>>

Recently Schuler \cite{Sch03} presented a randomized algorithm that solves SAT in expected time at most $2^{n(1-1/\log_2(2m))}$ up to a polynomial factor, where $n$ and $m$ are, respectively, the number of variables and the number of clauses in the input formula. This bound is the best known upper bound for testing ... more >>>

We present a simple randomized algorithm for SAT and prove an upper bound on its running time. Given a Boolean formula F in conjunctive normal form, the algorithm finds a satisfying assignment for F (if any) by repeating the following: Choose an assignment A at random and search for a ... more >>>