SAT 2004 START ConferenceManager    


Derandomization of Schuler’s Algorithm for SAT

Evgeny Dantsin and Alexander Wolpert

Presented at The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004


Abstract

Recently Schuler \cite{Sch03} presented a randomized algorithm that solves SAT in expected time $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 satisfiability of formulas in CNF with no restriction on clause length (for the case when $m$ is not too large comparing to $n$). We derandomize this algorithm using deterministic $k$-SAT algorithms based on search in Hamming balls, and we prove that our deterministic algorithm has the same upper bound on the running time as Schuler's randomized algorithm.


  
START Conference Manager (V2.47.2)
Maintainer: rrgerber@softconf.com