Exploiting partial knowledge of satisfying assignments

Recently Schöning has shown that a simple local-search algorithm for 3SAT achieves the currently best upper bound, i.e., an expected time of 1.334n1.334n. In this paper, we show that this algorithm can be modified to run much faster if there is some kind of imbalance in satisfying assignments and we have a (partial) knowledge about that. Especially if a satisfying assignment has imbalanced 0's and 1's, i.e., p1np1n 1's and (1-p1)n(1-p1)n 0's, then we can find a solution in time 1.260n1.260n when p1=13 and 1.072n1.072n when p1=0.1p1=0.1. Such an imbalance often exists in SAT instances reduced from other problems. As a concrete example, we investigate a reduction from 3DM and show our new approach is nontrivially faster than its direct algorithms. Preliminary experimental results are also given.