  It is well known that, as $n$ tends to infinity, the probability of
satisfiability for a random 2-SAT formula on $n$ variables, where each clause
occurs independently with probability $\alpha/2n$, exhibits a sharp threshold
at $\alpha=1$. We study a more general 2-SAT model in which each clause occurs
independently but with probability $\alpha_i/2n$ where $i \in \{0,1,2\}$ is the
number of positive literals in that clause. We generalize branching process
arguments by Verhoeven(99) to determine the satisfiability threshold for this
model in terms of the maximum eigenvalue of the branching matrix.
