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 literals
Daniele 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