LLL for k-SAT k-CNF of max degree d Theorem d≤2k-2 > 3 satisfying assignment for uniform random assignment X1,X2,...,Xn for clause Ci,bad event Ai:Ci is not satisfied LLL: e(d+1)≤2kE >0
Theorem d 2k2 ∃ satisfying assignment for φ e(d + 1) 2k for clause Ci , bad event Ai : uniform random assignment X1, X2,...,Xn Ci is not satisfied φ : k-CNF of max degree d LLL: Pr ⇤ n i=1 Ai ⇥ > 0 LLL for k-SAT
Algorithmic LLL k-CNF of max degree d with m clauses on n variables Theorem d≤2k-2 3 satisfying assignment for Theorem (Moser,2009) d<2k-3[ 〉 satisfying assignment can be found in O(n+km logm)w.h.p
satisfying assignment can be found in O(n + km logm) w.h.p. ∃ satisfying assignment for φ Algorithmic LLL Theorem d 2k2 Theorem (Moser, 2009) d < 2k3 φ : k-CNF of max degree d with m clauses on n variables
k-CNF of max degree d with m clauses on n variables Sove(Φ) pick a random assignment X1,X2,…,X; while 3 unsatisfied clause C Fix(C); Fix(C) replace variables in C with random values; while 3 unsatisfied clause D overlapping with C Fix(D);
Solve(φ) pick a random assignment x1, x2, ... , xn; while ∃ unsatisfied clause C Fix(C); Fix(C) replace variables in C with random values; while ∃ unsatisfied clause D overlapping with C Fix(D); φ : k-CNF of max degree d with m clauses on n variables
k-CNF of max degree d with mn clauses on n variables Solve() Fix(C) Pick a random assignment replace variables in C with random values; X1,x2,…,X: while 3 unsatisfied clause C while 3 unsatisfied clause D overlapping with C Fix(C); Fix(D); at top-level: Observation:A clause C is satisfied and will keep satisfied once it has been fixed. of top-level calls to Fix(C)<m(#of clauses) total of calls to Fix(C)(including recursive calls):t
Solve(φ) Pick a random assignment x1, x2, ... , xn; while ∃ unsatisfied clause C Fix(C); Fix(C) replace variables in C with random values; while ∃ unsatisfied clause D overlapping with C Fix(D); at top-level: Observation: A clause C is satisfied and will keep satisfied once it has been fixed. # of top-level calls to Fix(C) : ≤m (# of clauses) total # of calls to Fix(C) (including recursive calls): t φ : k-CNF of max degree d with m clauses on n variables
k-CNF of max degree d with m clauses on n variables Solve() Fix(C) Pick a random assignment replace variables in C with random values; X1,X2,…,X while 3 unsatisfied clause D overlapping with C while 3 unsatisfied clause C Fix(C); Fix(D); ≤n recursion trees total nodes:t total of random bits: n+tk (assigned bits) Observation: Fix(C)is called assignment of C is uniquely determined
≤m total # nodes: t Solve(φ) Pick a random assignment x1, x2, ... , xn; while ∃ unsatisfied clause C Fix(C); Fix(C) replace variables in C with random values; while ∃ unsatisfied clause D overlapping with C Fix(D); recursion trees total # of random bits: n+tk (assigned bits) Observation: Fix(C) is called assignment of C is uniquely determined φ : k-CNF of max degree d with m clauses on n variables