Investigating and improving the PPSZ algorithm for SAT
Timon Hertli · Repository for Publications and Research Data (ETH Zurich) · 2010
In this thesis, we give a self-contained analysis of the PPSZ algorithm [8], including the combination with Sch öning's algorithm [14] of Iwama and Tamaki [5] and the improvement of Rolf [13].We also give new bounds for 3-SAT and 4-SAT using the following idea: A critical variable of a satisfiable CNF formula is a variable that has the same value in all satisfying assignments.With a simple case distinction on the fraction of critical variables of a CNF formula, we improve the bound for 3-SAT from O(1.32216 n ) [13] to O(1.32153 n ).Using a different approach, Iwama et al. [4] very recently achieved a running time of O(1.32113 n ).Our method nicely combines with theirs, yielding an even faster algorithm with running time O(1.32065 n ).We also improve the bound for 4-SAT from O(1.47390 n ) [5] to O(1.46928 n ), where O(1.46981 n ) can be obtained using only the methods of [5] and [13].This is very close to the bound for unique 4-SAT for PPSZ, O(1.46899 n ) [8].i