Faster Random k-CNF Satisfiability
share
We describe an algorithm to solve the problem of Boolean CNF-Satisfiability when the input formula is chosen randomly. We build upon the algorithms of Schöning 1999 and Dantsin et al. in 2002. The Schöning algorithm works by trying many possible random assignments, and for each one searching systematically in the neighborhood of that assignment for a satisfying solution. Previous algorithms for this problem run in time O(2^n (1- Ω(1)/k)). Our improvement is simple: we count how many clauses are satisfied by each randomly sampled assignment, and only search in the neighborhoods of assignments with abnormally many satisfied clauses. We show that assignments like these are significantly more likely to be near a satisfying assignment. This improvement saves a factor of 2^n Ω(^2 k)/k, resulting in an overall runtime of O(2^n (1- Ω(^2 k)/k)) for random k-SAT.
READ FULL TEXT