Mick gets some (the odds are on his side) [satisfiability]

Consider a randomly generated boolean formula F (in the conjunctive normal form) with m clauses of size k over n variables; k is fixed at any value greater than 1, but n tends to infinity and m = (1 + o(1))cn for some c depending only on k. It is easy to see that F is unsatisfiable with probability 1-o(1) whenever c>(ln 2)2^k; the authors complement this observation by proving that F is satisfiable with probability 1-o(1) whenever c<(0.25)2^k/k; in fact, they present a linear-time algorithm that satisfies F with probability 1-o(1). In addition, they establish a threshold for 2-SAT: if k = 2 then F is satisfiable with probability 1-o(1) whenever c<1 and unsatisfiable with probability 1-o(1) whenever c>1