Phase Transition in Unrestricted Random SAT

TL;DR

This paper precisely determines the phase transition point in unrestricted random SAT problems, revealing a strong dependence on the number of variables and positive literals, differing from traditional K-SAT models.

Contribution

It provides an exact calculation of the satisfiability transition in unrestricted random SAT, showing the critical density depends exponentially on the number of positive literals.

Findings

Critical density ccr = ln(2)/(1-p)^n for large n

Second moment method successfully applied to unrestricted SAT

Transition line depends strongly on positive literal ratio

Abstract

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.