The Satisfiability Threshold for Non-Uniform Random 2-SAT

Abstract

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=\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}))$ 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].

51 pages, 6 figures, extended abstract appeared at ICALP 2019