RAIRO-Theor. Inf. Appl.
Volume 49, Number 1, January-March 2015
|Page(s)||23 - 45|
|Published online||23 February 2015|
Aix-Marseille Université, CNRS, LIF UMR 7279,
2 Aix-Marseille Université, CNRS, I2M UMR 7373, 13453 Marseille, France
3 Institut für Informationsysteme 184/3, Technische Universität Wien, Favoritenstrasse 9-11 A-1040 Wien, Austria
4 University Grenoble Alpes, IF, 38000 Grenoble, France
5 CNRS, IF, 38000 Grenoble, France
Received: 5 May 2014
Accepted: 28 August 2014
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.
Mathematics Subject Classification: 68R01 / 60C05 / 05A16
Key words: Random quantified formulas / satisfiability / phase transition / sharp threshold
© EDP Sciences 2015
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.