Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT

Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT

Tobias Friedrich, Ralf Rothenberger

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence
Best Sister Conferences. Pages 6151-6155. https://doi.org/10.24963/ijcai.2019/853

We study a more general model to generate random instances of Propositional Satisfiability (SAT) with n Boolean variables, m clauses, and exactly k variables per clause. Additionally, our model is given an arbitrary probability distribution (p_1, ..., p_n) on the variable occurrences. Therefore, we call it non-uniform random k-SAT. The number m of randomly drawn clauses at which random formulas go from asymptotically almost surely (a.a.s.) satisfiable to a.a.s. unsatisfiable is called the satisfiability threshold. Such a threshold is called sharp if it approaches a step function as n increases. We identify conditions on the variable probability distribution (p_1, ..., p_n) under which the satisfiability threshold is sharp if its position is already known asymptotically. This result generalizes Friedgut’s sharpness result from uniform to non-uniform random k -SAT and implies sharpness for thresholds of a wide range of random k -SAT models with heterogeneous probability distributions, for example such models where the variable probabilities follow a power-law.
Keywords:
Constraints and SAT: SAT: Evaluation and Analysis
Constraints and SAT: Modeling;Formulation