The Satisfiability Threshold for Non-Uniform Random 2-SAT

Propositional satisfiability (SAT) is one of the most fundamental problems in computer science. Its worst-case hardness lies at the core of computational complexity theory, for example in the form of NP-hardness and the (Strong) Exponential Time Hypothesis. In practice however, SAT instances can often be solved efficiently. This contradicting behavior has spawned interest in the average-case analysis of SAT and has triggered the development of sophisticated rigorous and non-rigorous techniques for analyzing random structures. Despite a long line of research and substantial progress, most theoretical work on random SAT assumes a uniform distribution on the variables. In contrast, real-world instances often exhibit large fluctuations in variable occurrence. This can be modeled by a non-uniform distribution of the variables, which can result in distributions closer to industrial SAT instances. We study satisfiability thresholds of non-uniform random $2$-SAT with $n$ variables and $m$ clauses and with an arbitrary probability distribution $(p_i)_{iin[n]}$ with $p_1 ge p_2 ge ldots ge p_n > 0$ over the n variables. We show for $p_1^2=Theta(sum_{i=1}^n p_i^2)$ that the asymptotic satisfiability threshold is at $m=Theta( (1-sum_{i=1}^n p_i^2)/(p_1cdot(sum_{i=2}^n p_i^2)^{1/2}) )$ and that it is coarse. For $p_1^2=o(sum_{i=1}^n p_i^2)$ we show that there is a sharp satisfiability threshold at $m=(sum_{i=1}^n p_i^2)^{-1}$. This result generalizes the seminal works by Chvatal and Reed [FOCS 1992] and by Goerdt [JCSS 1996].