The threshold for random (1,2)-QSAT

Abstract

The QSAT problem is the quantified version of the SAT problem. We show the existence of a threshold effect for the phase transition associated with the satisfiability of random quantified extended 2-CNF formulas. We consider boolean CNF formulas of the form $\forall X \exists Y φ(X,Y)$, where $X$ has $m$ variables, $Y$ has $n$ variables and each clause in $φ$ has one literal from $X$ and two from $Y$. For such formulas, we show that the threshold phenomenon is controlled by the ratio between the number of clauses and the number $n$ of existential variables. Then we give the exact location of the associated critical ratio $c^{*}$. Indeed, we prove that $c^{*}$ is a decreasing function of $ α$, where $α$ is the limiting value of $m / \log (n)$ when $n$ tends to infinity.

20 pages. Preliminary, conference versions of this article appeared in SAT08 and SAT09