Exact location of the phase transition for random (1,2)-QSAT^∗,∗∗

¹ Aix-Marseille Université, CNRS, LIF UMR 7279, 13288 Marseille, France
creignou@lif.univ-mrs.fr
² Aix-Marseille Université, CNRS, I2M UMR 7373, 13453 Marseille, France
daude@cmi.univ-mrs.fr
³ Institut für Informationsysteme 184/3, Technische Universität Wien, Favoritenstrasse 9-11 A-1040 Wien, Austria
uwe@kr.tuwien.ac.at
⁴ University Grenoble Alpes, IF, 38000 Grenoble, France
⁵ CNRS, IF, 38000 Grenoble, France
raphael.rossignol@ujf-grenoble.fr

Received: 5 May 2014
Accepted: 28 August 2014

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 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^∗: it is a decreasing function of α, where α is the limiting value of m/ log (n) when n tends to infinity. Thus we give a precise location of the phase transition associated with a coNP-complete problem.