2009/07/06 by Nadia Creignou, Creignou, Nadia, Herve Daude +5
Computer Science · #Discrete Mathematics (cs.DM) #FOS: Computer and information sciences #cs.DM
paper · pdf · doi:10.48550/arxiv.0907.0937
20 pages. Preliminary, conference versions of this article appeared in SAT08 and SAT09
arxiv created 2009/07/06 · arxiv updated 2009/12/01
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 ∀ X ∃ 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.