We construct k-CNFs with m variables on which the strong version of PPSZ kSAT algorithm, which uses bounded width resolution, has success probability at most 2 ?(1?(1 )2/k)m for every 0. Previously such a bound was known only for the weak PPSZ algorithm which exhaustively searches through small subformulas of the CNF to see if any of them forces the value of a given variable, and for strong PPSZ the best known previous upper bound was 2?(1?O(log(k)/k))m (Pudl′ak et al., ICALP 2017).
展开▼
