Algorithms for the Diverse-k-SAT Problem: The Geometry of Satisfying Assignments.

Given a k-CNF formula and an integer s ≥ 2, we study algorithms that obtain s solutions to the formula that are as dispersed as possible. For s = 2, this problem of computing the diameter of a k-CNF formula was initiated by Creszenzi and Rossi, who showed strong hardness results even for k = 2. The current best upper bound [Angelsmark and Thapper’04] goes to 4n as k → ∞. As our first result, we show that this quadratic blow up is not necessary by utilizing the Fast-Fourier transform (FFT) to give a O*(2n) time exact algorithm for computing the diameter of any k-CNF formula. For s > 2, the problem was raised in the SAT community (Nadel’11) and several heuristics have been proposed for it, but no algorithms with theoretical guarantees are known. We give exact algorithms using FFT and clique-finding that run in O*(2(s−1)n) and O*(s2|ΩF|ω⌈s/3⌉) respectively, where |ΩF| is the size of the solutions space of the formula F and ω is the matrix multiplication exponent. However, current SAT algorithms for finding one solution run in time O*(2εkn) for εk ≈ 1−Θ(1/k), which is much faster than all above run times. As our main result, we analyze two popular SAT algorithms - PPZ (Paturi, Pudlák, Zane’97) and Schöning’s (’02) algorithms, and show that in time poly(s)O*(2εkn), they can be used to approximate diameter as well as the dispersion (s > 2) problem. While we need to modify Schöning’s original algorithm for technical reasons, we show that the PPZ algorithm, without any modification, samples solutions in a geometric sense. We believe this geometric sampling property of PPZ may be of independent interest. Finally, we focus on diverse solutions to NP-complete optimization problems, and give bi-approximations running in time poly(s)O*(2εn) with ε < 1 for several problems such as Maximum Independent Set, Minimum Vertex Cover, Minimum Hitting Set, Feedback Vertex Set, Multicut on Trees and Interval Vertex Deletion. For all of these problems, all existing exact methods for finding optimal diverse solutions have a runtime with at least an exponential dependence on the number of solutions s. Our methods show that by relaxing to bi-approximations, this dependence on s can be made polynomial.