Delay of SAT-algorithms by Schuler and his derandomization by Dantsin and Wolpert
Wei Gong, Bin Lian · 2010
The satisfaction problem (SAT-problem) for propositional formulas one of the most common NP-hard problems: for a propositional formula F the problem is to determine if F is satisfiable or not. There are two groups of algorithms that can solve this problem - deterministic and randomized algorithms. In this proposal we will analyze two of the most common algorithms, the randomized algorithm by Rainer Schuler and its derandomization by Evgeny Dantsin and Alexander Wolpert. Both theoretical have the delay of equation with a polynomial p, n as the number of variables in the formula and m as the number of clauses in the formula. But there is no practical analysis and this will show you here. The explanation of these algorithms is not part of this work. First of all some notations will be introduced. A clause K is the disjunction of literals. A formula F is a propositional formula in conjunctive normal form (CNF). A configuration of the variables x1,...,xn is a map to logical value. The number of variable in a formula is n and the number of clauses in a formula is m.