Algorithms for SAT Based on Search in Hamming Balls.pptVIP

Algorithms for SAT Based on Search in Hamming Balls Author : Evgeny Dantsin, Edward A. Hirsch, and Alexander Wolpert Speaker : 張經略, 吳冠賢, 羅正偉 Outline Introduction Definitions and notation Randomized Algorithm Derandomization Introduction In this paper a randomized algorithm for SAT is given, and its derandomized version is the first non-trivial bound for a deterministic SAT algorithm with no restriction on clause length. For k-SAT, Schuler’s algorithm is better than this one. Notation Fact about H The graph of H is A bound of V(n,R) Ball-Checking algorithms Observations The recursion depth is at most R Any literal is altered at most once during execution of Ball-Checking, and at any time, those remaining variables are assigned as in the original assignment Lemma 1 There is a satisfying assignment in B(A,R) iff Ball-Checking(F,A,R) returns a satisfying assignment in B(A,R) Proof. The lemma is correct for R=0. For the induction step, assume that Ball-Checking(Fi,Ai,R-1) finds a satisfying assignment in B(Ai,R-1), if any. Furthermore, the assignment found can be different from Ai only at those variables that appear in Fi. Lemma2 The running time of Ball-Checking(F,A,R) is at most , where k is the maximum length of clauses occurring at step 3 in all recursive calls. Proof. The recursion depth is at most R and the maximum degree of branching is at most k. Full Ball Checking Procedure Full-Ball-Checking(F,A,R)Input: formula F over variables assignment A, number ROutput: satisfying assignment or “no” 1.Try each assignment A’ in B(A,R), if it satisfies F, return it. 2.Return “no” Observation Full-Ball-Checking runs in time poly(n)mV(n,R) Randomized algorithm Correctness Lemma 3. For any R,l,(a)If F is unsatisfiable, then Random-Balls returns “no”, (b)else Random-Balls finds a satisfying assignment with probabability 1/2 Proofs of lemma 3 Amplifying prob. of correctness Choosing N to be n time larger will reduce the probabilit