arXiv2026
The PPSZ algorithm of Paturi, Pudlák, Saks, and Zane solves 3-SAT by processing the variables in a uniformly random order, setting a variable whenever a bounded number of clauses implies its value, and guessing it otherwise. Its running time is determined by how many variables are forced in this process, and the exact exponent is a central question in the study of exponential-time satisfiability algorithms. Scheder showed that the classical analysis of PPSZ is not tight for 3-SAT. We ask how much further a sharper analysis of the unmodified algorithm can go. Our analysis uses auxiliary distributions on variable orderings that correlate the positions of variables sharing critical clauses. Such correlations make forcing more likely for some variables, can make it less likely for others, and incur an entropy cost. We choose the correlated pairs at random on short components, so that every pair is selected with the same probability, and we express the forcing loss as a sum of weights attached to these pairs in advance. Gains and losses then scale by the same factor and can be compared directly. Combining the resulting estimate with the complementary estimate of Scheder through an explicit linear-programming certificate gives a uniform improvement for every uniquely satisfiable formula. We prove that the original PPSZ algorithm, with a sufficiently large but fixed implication strength, solves Unique-3-SAT in randomized time $O^*(1.306969598^n)$. Through the lifting framework of Scheder and Steinberger, it solves general 3-SAT in randomized time $O^*(1.307031578^n)$. Both bounds improve the guarantees obtained from the analysis of Scheder for the same algorithm. These improvements follow entirely from the analysis, while PPSZ continues to use a uniformly random variable order and unbiased guesses. It shows that the known guarantees for PPSZ can be strengthened by analysis alone.