Skip to main content
Log in

Regular Random k-SAT: Properties of Balanced Formulas

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  • Achlioptas, D. (2001): Lower bounds for random 3-SAT via differential equations, Theor. Comp. Sci. 265, pp. 159–185.

    Article  MATH  MathSciNet  Google Scholar 

  • 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.

  • Achlioptas, D. and Peres, Y. (2004): The threshold for random k-SAT is 2k ln2 –O(k), J. Amer. Math. Soc. 17, 947–973.

    Article  MATH  MathSciNet  Google Scholar 

  • 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.

  • 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.

  • Bollobas, B. (2001): Random Graphs Second Edition, Cambridge University Press, United Kingdom.

    Google Scholar 

  • Chvatal, V. and Reed, B. (1992): Mick gets some (the odds are on his side). Proceedings of 33rd FOCS, pp. 620–627.

  • Chvatal, V. and Szemeredi, E. (1988): Many hard examples for resolution, J. Assoc. Comput. Mach. 35 759–768.

    MATH  MathSciNet  Google Scholar 

  • 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.

  • Dubois, O. (2001): Upper bounds on the satisfiability threshold, Theor. Comput. Sci. Vol. 265, 187–197.

    Article  MATH  Google Scholar 

  • 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.

    Article  MATH  MathSciNet  Google Scholar 

  • 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.

  • 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).

  • Fernandez de la Vega, W. (1992): On random 2-SAT. Manuscript.

  • Friedgut, E. (1999): Sharp thresholds for graph properties and the k-sat problem, J. Amer. Math. Soc. 12, 1017–1054.

    Article  MATH  MathSciNet  Google Scholar 

  • Goerdt, A. (1996): A threshold for unsatisfiability, J. Comput. Syst. Sci. 53(3), 469–486.

    Article  MATH  MathSciNet  Google Scholar 

  • Hajiaghayi, M. and Sorkin, G. (2004) The satisfiability threshold of random 3-SAT is at least 3.52. www.math.mit.edu/hajiagha/3satRCl.ps.

  • Janson, S., Luczak, T. and Rucinski, A. (2002): Random Graphs, Wiley, New York.

    MATH  Google Scholar 

  • 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.

  • Kaporis, A. C., Kirousis, L. M. and Lalas, E. (2003): Selecting complementary pairs of literals. Electron. Notes Discrete Mathem. 16.

  • 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.

  • 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.

    Article  MATH  MathSciNet  Google Scholar 

  • Le Berre, D. and Simon, L. (2004): SAT competitions. http://www.lri.fr/simon/contest/results/

  • Li, C.-M.: SATZ. http://www.laria.u-picardie.fr/cli/EnglishPage.html.

  • 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.

  • Wormald, N. C. (1995): Differential equations for random processes and random graphs, Ann. Appl. Probab. 5(4), 1217–1235.

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Yacine Boufkhad.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Boufkhad, Y., Dubois, O., Interian, Y. et al. Regular Random k-SAT: Properties of Balanced Formulas. J Autom Reasoning 35, 181–200 (2005). https://doi.org/10.1007/s10817-005-9012-z

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-005-9012-z

Key words

Navigation