Journal of Automated Reasoning

, Volume 35, Issue 1–3, pp 181–200 | Cite as

Regular Random k-SAT: Properties of Balanced Formulas

  • Yacine Boufkhad
  • Olivier Dubois
  • Yannet Interian
  • Bart Selman


We consider a model for generating random k-SAT formulas, in which each literal occurs approximately the same number of times in the formula clauses (regular random and k-SAT). Our experimental results show that such regular random k-SAT instances are much harder than the usual uniform random k-SAT problems. This is in agreement with other results that show that more balanced instances of random combinatorial problems are often much more difficult to solve than uniformly random instances, even at phase transition boundaries. There are almost no formal results known for such problem distributions. The balancing constraints add a dependency between variables that complicates a standard analysis. Regular random 3-SAT exhibits a phase transition as a function of the ratio α of clauses to variables. The transition takes place at approximately α = 3.5. We show that for α > 3.78  with high probability (w.h.p.) random regular 3-SAT formulas are unsatisfiable. Specifically, the events \({\user1{\mathcal{E}}}_{n} \) hold with high probability if Pr \({\left( {{\user1{\mathcal{E}}}_{n} } \right)} \to 1\) when n → ∞. We also show that the analysis of a greedy algorithm proposed by Kaporis et al. for the uniform 3-SAT model can be adapted for regular random 3-SAT. In particular, we show that for formulas with ratio α < 2.46, a greedy algorithm finds a satisfying assignment with positive probability.

Key words

satisfiability phase transition k-SAT regular Boolean formulae 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Achlioptas, D. (2001): Lower bounds for random 3-SAT via differential equations, Theor. Comp. Sci. 265, pp. 159–185.MATHCrossRefMathSciNetGoogle Scholar
  2. Achlioptas, D. and Moore, C. (2002): The asymptotic order of the random k-SAT threshold, in 43th Annual Symposium on Foundations of Computer Science, Vancouver, pp. 779–788.Google Scholar
  3. Achlioptas, D. and Peres, Y. (2004): The threshold for random k-SAT is 2k ln2 –O(k), J. Amer. Math. Soc. 17, 947–973.MATHCrossRefMathSciNetGoogle Scholar
  4. Achlioptas, D., Gomes, C. P., Kautz, H. A., and Selman, B. (2000): Generating satisfiable problems instances, in Proceedings of 17th National Conference on Artificial Intelligence, pp. 256–261.Google Scholar
  5. Bayardo, R. J. and Schrag, R. (1996): Using CSP look-back techniques to solve exceptionally hard SAT instances, in Proceedings of the Second Int. Conf. on Principles and Practice of Constraint Programming, pp. 46–60.Google Scholar
  6. Bollobas, B. (2001): Random Graphs Second Edition, Cambridge University Press, United Kingdom.Google Scholar
  7. Chvatal, V. and Reed, B. (1992): Mick gets some (the odds are on his side). Proceedings of 33rd FOCS, pp. 620–627.Google Scholar
  8. Chvatal, V. and Szemeredi, E. (1988): Many hard examples for resolution, J. Assoc. Comput. Mach. 35 759–768.MATHMathSciNetGoogle Scholar
  9. Cooper, C., Frieze, A. and Sorkin, G. B. (2002): A note on random 2-SAT with prescribed literal degrees. Proceedings of the 13th Annual ACM-SIAM Symposium on Discrete Algorithms.Google Scholar
  10. Dubois, O. (2001): Upper bounds on the satisfiability threshold, Theor. Comput. Sci. Vol. 265, 187–197.MATHCrossRefGoogle Scholar
  11. Dubois, O. and Boufkhad, Y. (1997): A general upper bound for the satisfiability threshold of random r-SAT formulae, J. Algorithms 24(2), 395–420.MATHCrossRefMathSciNetGoogle Scholar
  12. Dubois, O. and Dequen, G. (2001): A backbone search heuristic for efficient solving of hard 3-SAT formulae, in Proceedings of 17th International Joint Conference on Artificial Intelligence, Seattle, pp. 248–253.Google Scholar
  13. Dubois, O., Boufkhad, Y. and Mandler, J. (2000): Typical random 3-SAT formulae and the satisfiability threshold, in SODA, pp. 126–127. Full version in Electronic Colloquium on Computational Complexity (ECCC 2003).Google Scholar
  14. Fernandez de la Vega, W. (1992): On random 2-SAT. Manuscript.Google Scholar
  15. Friedgut, E. (1999): Sharp thresholds for graph properties and the k-sat problem, J. Amer. Math. Soc. 12, 1017–1054.MATHCrossRefMathSciNetGoogle Scholar
  16. Goerdt, A. (1996): A threshold for unsatisfiability, J. Comput. Syst. Sci. 53(3), 469–486.MATHCrossRefMathSciNetGoogle Scholar
  17. Hajiaghayi, M. and Sorkin, G. (2004) The satisfiability threshold of random 3-SAT is at least 3.52.
  18. Janson, S., Luczak, T. and Rucinski, A. (2002): Random Graphs, Wiley, New York.MATHGoogle Scholar
  19. Kaporis, A. C., Kirousis, L. M. and Lalas, E. G. (2002): The probabilistic analysis of a greedy satisfiability algorithm, in 10th Annual European Symposium on Algorithms.Google Scholar
  20. Kaporis, A. C., Kirousis, L. M. and Lalas, E. (2003): Selecting complementary pairs of literals. Electron. Notes Discrete Mathem. 16.Google Scholar
  21. Kautz, H., Ruan, Y., Achlioptas, D., Gomes, C. P., Selman, B. and Stickel, M. (2001): Balance and filtering in structured satisfiable problems, in Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence.Google Scholar
  22. Kirousis, L. M., Kranakis, E., Krizanc, D. and Stamatiou, Y. C. (1998): Approximating the unsatisfiability threshold of random formulas, Random Struct. Algorithms 12(3), 253–269.MATHCrossRefMathSciNetGoogle Scholar
  23. Le Berre, D. and Simon, L. (2004): SAT competitions.
  24. Mitchell, D., Selman, B. and Levesque, H. (1992): Hard and easy distributions of SAT problems, in Proceedings of the 10th National Conf. on Artificial Intelligence, pp. 459–465.Google Scholar
  25. Wormald, N. C. (1995): Differential equations for random processes and random graphs, Ann. Appl. Probab. 5(4), 1217–1235.MATHMathSciNetGoogle Scholar

Copyright information

© Springer Science+Business Media, Inc. 2006

Authors and Affiliations

  • Yacine Boufkhad
    • 1
  • Olivier Dubois
    • 2
  • Yannet Interian
    • 3
  • Bart Selman
    • 4
  1. 1.LIAFACNRS-Université Denis Diderot- Case 7014Paris Cedex 05France
  2. 2.LIP6, Box 169CNRS-Université Paris 6Paris Cedex 05France
  3. 3.Center for Applied MathematicsCornell UniversityIthacaUSA
  4. 4.Depatiment of Computer ScienceCornell UniversityIthacaUSA

Personalised recommendations