Solving Non-Uniform Planted and Filtered Random SAT Formulas Greedily

Conference: International Conference on Theory and Applications of Satisfiability Testing 2021

Speaker: Ralf Rothenberger

Abstract: Recently, there has been an interest in studying non-uniform random k-satisfiability (k-SAT) models in order to address the non-uniformity of formulas arising from real-world applications. While uniform random k-SAT has been extensively studied from both a theoretical and experimental perspective, understanding the algorithmic complexity of heterogeneous distributions is still an open challenge. When a sufficiently dense formula is guaranteed to be satisfiable by conditioning or a planted assignment, it is well-known that uniform random k-SAT is easy on average. We generalize this result to the broad class of non-uniform random k-SAT models that are characterized only by an ensemble of distributions over variables with a mild balancing condition. This balancing condition rules out extremely skewed distributions in which nearly half the variables occur less frequently than a small constant fraction of the most frequent variables, but generalizes recently studied non-uniform k-SAT distributions such as power-law and geometric formulas. We show that for all formulas generated from this model of at least logarithmic densities, a simple greedy algorithm can find a solution with high probability.
As a side result we show that the total variation distance between planted and filtered (conditioned on satisfiability) models is o(1) once the planted model produces formulas with a unique solution with probability 1-o(1). This holds for all random k-SAT models where the signs of variables are drawn uniformly and independently at random.

This is joined work with Tobias Friedrich, Frank Neumann and Andrew M. Sutton.