  For random CNF formulae with m clauses, n variables and an unrestricted
number of literals per clause the transition from high to low satisfiability
can be determined exactly for large n. The critical density m/n turns out to be
strongly n-dependent, ccr = ln(2)/(1-p)^^n, where pn is the mean number of
positive literals per clause.This is in contrast to restricted random SAT
problems (random K-SAT), where the critical ratio m/n is a constant. All
transition lines are calculated by the second moment method applied to the
number of solutions N of a formula. In contrast to random K-SAT, the method
does not fail for the unrestricted model, because long range interactions
between solutions are not cut off by disorder.
