Delay of SAT-Algorithms by Schuler and his Derandomization by Dantsin and Wolpert
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 O(p ? 2~(n(1-1/log_2~(23))) ) 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 xl,….,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.
deterministic algorithms randomized algorithms satisfiable formulas non-satisfiable formulas
Wei Gong Bin Lian
The department of electronic & information Tianjin institute of urban construction Tianjin, China
国际会议
太原
英文
430-433
2010-10-22（万方平台首次上网日期，不代表论文的发表时间）