2 major cases to consider at the moment are the promise problem unique k-SAT and Affine-2-SAT, perhaps even 3Affine-2-SAT.

PPSZ(F in k-CNF, d >= 1) perform k^d bounded resolution on F choose permutation pi of var(F) at random choose bit string b of length n=|var(F)| at random for i=1 to n if F contains a unit clause in xi, set xi as it must be else set xi as bi simplify F by removing true clauses and false literalsDaniele Rolf derandomized the above algorithm [DR05] by replacing the choice of the permutation by a pseudo random permutation using a small number of random bits. The random bits used for the pseudo random permutation and the random bits used for b are then replaced by exhaustive search.

The pseudo random permutation was chosen to closly match the analysis of [PPSZ98], which chose n independent and uniformly random variables over the unit interval, and considered the permutation induced by their order. Since the sample space is continuous, the analysis could involve integration.

[DR05] approximates this continuous sample space with a discrete version with L bits of accuracy; so instead of uniform random variables over (0,1), we now have uniform variables over {i / 2^L | 0 <= i < 2^L}. Furthermore, only w-wise independent random variables are needed, where w depends only on k,d (not n). This is because we only need the order according to pi of the variables that appear as labels of critical clause trees to be fully random, and a critical clause tree only has size <= w=(k-1)^(d+1)-1 (actually ((k-1)^(d+1)-1)/(k-2), but it's not important). Very little accuracy is lost in the discretization, and hence almost the same analysis carries through.

However, to construct the sample space requires polytime in the size of the sample space, which has size O(n^(Lw/2)), where w depends only on k,d and L is another approximation parameter. To get a good approximation, L may need to be large, and hence the exponent in the polynomial may be large. So this derandomized algorithm may not be as tractable as the original [PPSZ98] algorithm, although the original [PPSZ98] algorithm was already pretty slow due to the initial k^d-bounded resolution step.

(=>) Suppose that forall a in 2^n-S, exists v_a subset n, |v_a|<=k s.t. forall b in S a|v_a!=b|v_a. If p is a partial assignment to k' variables, let C_p denote the k'-clause that is false exactly at p. Let F={C_(a|v_a) | a in 2^n-S}. We claim that F interpolates S.

F rejects all a in 2^n-S since the clause C_(a|v_a)(a)=0. Now suppose indirectly that F rejects some b in S. Then exists a in 2^n-S s.t. C_(a|v_a)(b)=0=C_(a|v_a)(a). But a|v_a!=b|v_a, so the above equation is impossible. QED

**Corollary 2:**
Every subset S of 2^n of size s<=k is the
solution space of some k-CNF.

**Proof:**
We apply the theorem.
Let a in 2^n-S.
Then forall b in S, exists i_b in n s.t. a(i_b)!=b(i_b).
Let v={i_b | b in S}. Then |v|<=k
and forall b in S, a|v!=b|v.
So S is interpolable.
QED

**Corollary 3:**
There is a subset S of 2^n of size k+1 that is not interpolable
by a k-CNF (provided n>k).

**Proof:**
We apply the theorem.
Let S be the rows of the k+1 by k+1 identity matrix.
Set a = 0^n.
Then forall v subset n with |v|<=k, exists i in (k+1)-v.
So row i of the identity matrix agrees with a on the
columns in v.
So S is not interpolable.
QED

**DR05**- D. Rolf.

Derandomization of PPSZ for Unique-k-SAT,

To appear in the Springer LNCS volume proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT-2005), June 19th-23rd 2005. **PPSZ98**- R. Paturi, P. Pudlak, M. Saks, and F. Zane.

An improved exponentialtime algorithm for k-SAT,

In Proceedings of the 39th IEEE Conference on Foundations of Computer Science, pages 628-637, 1998.