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

Creignou, Nadia; Daudé, Hervé; Egly, Uwe; Rossignol, Raphaël

doi:10.1051/ita/2014025

Creignou, Nadia ¹ ; Daudé, Hervé ² ; Egly, Uwe ³ ; Rossignol, Raphaël ^4,⁵

¹ Aix-Marseille Université, CNRS, LIF UMR 7279, 13288 Marseille, France
² Aix-Marseille Université, CNRS, I2M UMR 7373, 13453 Marseille, France
³ Institut für Informationsysteme 184/3, Technische Universität Wien, Favoritenstrasse 9-11 A-1040 Wien, Austria
⁴ University Grenoble Alpes, IF, 38000 Grenoble, France
⁵ CNRS, IF, 38000 Grenoble, France

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 49 (2015) no. 1, pp. 23-45.

Résumé

The $Q S A T$ problem is the quantified version of the $S A T$ 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 $\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^{*}$ : it is a decreasing function of $α$ , where $α$ is the limiting value of $m / l o g (n)$ when $n$ tends to infinity. Thus we give a precise location of the phase transition associated with a $c o N P$ -complete problem.

Reçu le : 2014-05-05
Accepté le : 2014-08-28

MR Zbl

DOI : 10.1051/ita/2014025

Classification : 68R01, 60C05, 05A16
Mots-clés : Random quantified formulas, satisfiability, phase transition, sharp threshold

Affiliations des auteurs :

Creignou, Nadia ¹ ; Daudé, Hervé ² ; Egly, Uwe ³ ; Rossignol, Raphaël ^{4, 5}

@article{ITA_2015__49_1_23_0,
     author = {Creignou, Nadia and Daud\'e, Herv\'e and Egly, Uwe and Rossignol, Rapha\"el},
     title = {Exact location of the phase transition for random {(1,2)-QSAT}},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {23--45},
     publisher = {EDP-Sciences},
     volume = {49},
     number = {1},
     year = {2015},
     doi = {10.1051/ita/2014025},
     mrnumber = {3342171},
     zbl = {1327.68129},
     language = {en},
     url = {http://archive.numdam.org/articles/10.1051/ita/2014025/}
}

TY  - JOUR
AU  - Creignou, Nadia
AU  - Daudé, Hervé
AU  - Egly, Uwe
AU  - Rossignol, Raphaël
TI  - Exact location of the phase transition for random (1,2)-QSAT
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2015
SP  - 23
EP  - 45
VL  - 49
IS  - 1
PB  - EDP-Sciences
UR  - http://archive.numdam.org/articles/10.1051/ita/2014025/
DO  - 10.1051/ita/2014025
LA  - en
ID  - ITA_2015__49_1_23_0
ER  -

%0 Journal Article
%A Creignou, Nadia
%A Daudé, Hervé
%A Egly, Uwe
%A Rossignol, Raphaël
%T Exact location of the phase transition for random (1,2)-QSAT
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2015
%P 23-45
%V 49
%N 1
%I EDP-Sciences
%U http://archive.numdam.org/articles/10.1051/ita/2014025/
%R 10.1051/ita/2014025
%G en
%F ITA_2015__49_1_23_0

Creignou, Nadia; Daudé, Hervé; Egly, Uwe; Rossignol, Raphaël. Exact location of the phase transition for random (1,2)-QSAT. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 49 (2015) no. 1, pp. 23-45. doi : 10.1051/ita/2014025. http://archive.numdam.org/articles/10.1051/ita/2014025/

Bibliographie
Cité par

B. Aspvall, M.F. Plass and R.E. Tarjan, A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inform. Process. Lett. 8 (1979) 121–123. | DOI | MR | Zbl

B. Bollobás, C. Borgs, J.T. Chayes, J.H. Kim and D.B. Wilson, The scaling window of the 2-SAT transition. Random Structures and Algorithms 18 (2001) 201–256. | DOI | MR | Zbl

H. Chen and Y. Interian, A model for generating random quantified boolean formulas. In Proc. of the 19th International joint Conference on Artificial Intelligence (IJCAI 2005) (2005) 66–71.

V. Chvátal and B. Reed, Mick gets some (the odds are on his side). In Proc. of the 33rd Annual Symposium on Foundations of Computer Science (FOCS 92) (1992) 620–627. | Zbl

N. Creignou, H. Daudé and U. Egly, Phase transition for random quantified XOR-formulas. J. Artif. Intell. Res. 19 (2007) 1–18. | DOI | MR | Zbl

N. Creignou, H. Daudé, U. Egly and R. Rossignol, New results on the phase transition for random quantified Boolean formulas. Proc. of the 11th International Conference on Theory and Applications of Satisfiability Testing (SAT 2008). In vol. 4996 of Lect. Notes Comput. Sci. (2008) 34–47. | MR | Zbl

N. Creignou, H. Daudé, U. Egly and R. Rossignol, (1,2)-QSAT: A good candidate for understanding phase transitions mechanisms. Proc. of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009). In vol. 5584 of Lect. Notes Comput. Sci. (2009) 363–376. | MR

W. Fernandez De La Vega, Random 2-SAT: results and problems. Theor. Comput. Sci. 265 (2001) 131–146. | DOI | MR | Zbl

O. Dubois and Y. Boufkhad, A general upper bound for the satisfiability threshold of random r-SAT formulae. J. Algorithms 24 (1997) 395–420. | DOI | MR | Zbl

U. Egly, T. Eiter, H. Tompits and S. Woltran, Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas. In Proc. of the 17th National Conference on Artificial Intelligence and the 12th Innovative Applications of Artificial Intelligence Conference (AAAI/IAAI 2000). AAAI Press / MIT Press (2000) 417–422.

A. Flögel, M. Karpinski and H. Kleine Büning, Subclasses of quantified Boolean formulas. In Proceedings of the 4th Workshop on Computer Science Logic (CSL 90) (1990) 145–155. | MR

I.P. Gent and T. Walsh, Beyond NP: the QSAT phase transition. In Proc. of AAAI-99 (1999).

A. Goerdt, A threshold for unsatisfiability. J. Comput. Syst. Sci. 53 (1996) 469–486. | DOI | MR | Zbl

S. Janson, T. Luczack and A. Rucinski, Random graphs. John Wiley (2000). | MR | Zbl

B. Selman, D. Mitchell and H.J. Levesque, Generating hard satisfiability problems. Artif. Intell. 81 (1996) 17–29. | DOI | MR

N.M. Temme, Asymptotic estimates of Stirling numbers. Stud. Appl. Math. 89 (1993) 223–243. | DOI | MR | Zbl

Y. Verhoeven, Random 2-SAT and unsatisfiability. Inform. Proc. Lett. 72 (1999) 119–123. | DOI | MR | Zbl

D.B. Wilson, On the critical exponents of random $k$ -SAT. Random Struct. Algorithms 21 (2002) 182–195. | DOI | MR | Zbl

Cité par Sources :