  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 \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_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].
