Satisfiability threshold for random XOR-CNF formulas Original Research Article

Various experimental investigations have shown a sharp transition between satisfiability and unsatisfiability of CNF formulas with L clauses over n variables as c=L/n is varied. For 2-SAT it has been shown theoretically that a threshold phenomenon occurs at the critical value c=1. For 3-SAT experimental results show a sharp transition near c=4 but no such threshold phenomenon has already been proved. Noticing that the XOR-SAT problem (in which one uses the ‘exclusive or’ instead of the usual ‘or’) is a special case of satisfiability which is solvable in polynomial time as decision problem as well as counting problem leads to the natural question: is there a satisfiability threshold for XOR-SAT? In this paper, we answer this question in establishing a threshold phenomenon for XOR-SAT, with associated critical value c=1. So, consider randomly generated XOR-CNF formulas F. We prove that F is satisfiable with probability 1−o(1) whenever c<1 and unsatisfiable with probability 1−o(1) whenever c>1 as n tends to infinity. Indeed, in following the nice terminology classification given by Erdös and Rényi for random graphs, we obtain much better: we exhibit a probability distribution function that gives a complete understanding of the transition from satisfiability to unsatisfiability for random XOR-SAT formulas.