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{)}_{i\in [n]}$ with $p_1\ge p_2\ge \dots \ge p_n>0$ over the n variables. We show for $p_1^2=\mathrm{\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_1\cdot(\sum_{i=2}^n p_i^2)^{1/2}) )$andthatitiscoarse\mathrm{.}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].