Solving Non-uniform Planted and Filtered Random SAT Formulas Greedily

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.

Automated summary

Recent interest has been in studying non-uniform random k-SAT models to address the non-uniformity of formulas in real-world applications, challenging the algorithmic complexity of heterogeneous distributions. It is known that dense formulas guaranteed to be satisfiable are easy on average. A broad class of non-uniform random k-SAT models are characterized by distributions over variables that satisfy a balancing condition.