Faster Random k-CNF Satisfiability

Authors Andrea Lincoln, Adam Yedidia



PDF
Thumbnail PDF

File

LIPIcs.ICALP.2020.78.pdf
  • Filesize: 0.61 MB
  • 12 pages

Document Identifiers

Author Details

Andrea Lincoln
  • MIT, Cambridge, MA, USA
Adam Yedidia
  • MIT, Cambridge, MA, USA

Acknowledgements

We are very grateful to Greg Valiant, Virginia Williams, and Nikhil Vyas for their helpful conversations and kind support. Additionally, we are very appreciative of the email correspondence we had with Amin Coja-Oghlan, Allan Sly, and Nike Sun, who answered our many questions. We would also like to thank reviewers for their comments and suggestions. We would especially like to thank an exceptionally detailed and helpful review that we received on our paper last year.

Cite As Get BibTex

Andrea Lincoln and Adam Yedidia. Faster Random k-CNF Satisfiability. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 78:1-78:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.ICALP.2020.78

Abstract

We describe an algorithm to solve the problem of Boolean CNF-Satisfiability when the input formula is chosen randomly. 
We build upon the algorithms of Schöning 1999 and Dantsin et al. in 2002. The Schöning algorithm works by trying many possible random assignments, and for each one searching systematically in the neighborhood of that assignment for a satisfying solution. Previous algorithms for this problem run in time O(2^(n (1- Ω(1)/k))).
Our improvement is simple: we count how many clauses are satisfied by each randomly sampled assignment, and only search in the neighborhoods of assignments with abnormally many satisfied clauses. We show that assignments like these are significantly more likely to be near a satisfying assignment. This improvement saves a factor of 2^(n Ω(lg² k)/k), resulting in an overall runtime of O(2^(n (1- Ω(lg² k)/k))) for random k-SAT.

Subject Classification

ACM Subject Classification
  • Theory of computation → Random search heuristics
Keywords
  • Random k-SAT
  • Average-Case
  • Algorithms

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Scott Aaronson. P=?NP. Electronic Colloquium on Computational Complexity (ECCC), 24:4, 2017. URL: https://eccc.weizmann.ac.il/report/2017/004.
  2. D. Achioptas and G. B. Sorkin. Optimal myopic algorithms for random 3-sat. In Proceedings 41st Annual Symposium on Foundations of Computer Science, pages 590-600, November 2000. URL: https://doi.org/10.1109/SFCS.2000.892327.
  3. Dimitris Achlioptas. Random satisfiability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 245-270. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-245.
  4. Dimitris Achlioptas and Amin Coja-Oghlan. Algorithmic barriers from phase transitions. In 49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008, October 25-28, 2008, Philadelphia, PA, USA, pages 793-802, 2008. URL: https://doi.org/10.1109/FOCS.2008.11.
  5. Sarah R. Allen, Ryan O'Donnell, and David Witmer. How to refute a random CSP. In IEEE 56th Annual Symposium on Foundations of Computer Science, FOCS 2015, Berkeley, CA, USA, 17-20 October, 2015, pages 689-708, 2015. URL: https://doi.org/10.1109/FOCS.2015.48.
  6. Eli Ben-Sasson, Yonatan Bilu, and Danny Gutfreund. Finding a randomly planted assignment in a random 3CNF. Technical report, In preparation, 2002. Google Scholar
  7. Amin Coja-Oghlan. A better algorithm for random k-SAT. SIAM Journal on Computing, 39(7):2823-2864, 2010. Google Scholar
  8. Amin Coja-Oghlan, Colin Cooper, and Alan M. Frieze. An efficient sparse regularity concept. SIAM J. Discrete Math., 23(4):2000-2034, 2010. URL: https://doi.org/10.1137/080730160.
  9. Amin Coja-Oghlan, Andreas Goerdt, and André Lanka. Strong refutation heuristics for random k-sat. Combinatorics, Probability & Computing, 16(1):5-28, 2007. URL: https://doi.org/10.1017/S096354830600784X.
  10. Amin Coja-Oghlan, Michael Krivelevich, and Dan Vilenchik. Why almost all k-CNF formulas are easy. In Proceedings of the 13th International Conference on Analysis of Algorithms, to appear, 2007. Google Scholar
  11. Amin Coja-Oghlan and Konstantinos Panagiotou. The asymptotic k-SAT threshold. Advances in Mathematics, 288:985-1068, 2016. URL: https://doi.org/10.1016/j.aim.2015.11.007.
  12. Stephen A. Cook. The complexity of theorem-proving procedures. In Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pages 151-158, 1971. URL: https://doi.org/10.1145/800157.805047.
  13. Stephen A Cook and David G Mitchell. Finding hard instances of the satisfiability problem. In Satisfiability Problem: Theory and Applications: DIMACS Workshop, volume 35, pages 1-17, 1997. Google Scholar
  14. Evgeny Dantsin, Andreas Goerdt, Edward A. Hirsch, Ravi Kannan, Jon M. Kleinberg, Christos H. Papadimitriou, Prabhakar Raghavan, and Uwe Schöning. A deterministic (2-2/(k+1))^n algorithm for k-SAT based on local search. Theor. Comput. Sci., 289(1):69-83, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00174-8.
  15. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  16. Jian Ding, Allan Sly, and Nike Sun. Proof of the Satisfiability Conjecture for large k. In Proceedings of the Forty-Seventh Annual ACM on Symposium on Theory of Computing, STOC 2015, Portland, OR, USA, June 14-17, 2015, pages 59-68, 2015. URL: https://doi.org/10.1145/2746539.2746619.
  17. Olivier Dubois, Yacine Boufkhad, and Jacques Mandler. Typical random 3-sat formulae and the satisfiability threshold. In Proceedings of the Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, SODA '00, pages 126-127, Philadelphia, PA, USA, 2000. Society for Industrial and Applied Mathematics. URL: http://dl.acm.org/citation.cfm?id=338219.338243.
  18. Vitaly Feldman, Will Perkins, and Santosh Vempala. On the complexity of random satisfiability problems with planted solutions. Electronic Colloquium on Computational Complexity (ECCC), 21:148, 2014. URL: http://eccc.hpi-web.de/report/2014/148.
  19. Jun Gu, Paul W. Purdom, John Franco, and Benjamin W. Wah. Algorithms for the satisfiability (SAT) problem: A survey. In Satisfiability Problem: Theory and Applications, Proceedings of a DIMACS Workshop, Piscataway, New Jersey, USA, March 11-13, 1996, pages 19-152, 1996. URL: https://doi.org/10.1090/dimacs/035/02.
  20. Hiêp Hàn, Yury Person, and Mathias Schacht. Note on strong refutation algorithms for random k-sat formulas. Electronic Notes in Discrete Mathematics, 35:157-162, 2009. URL: https://doi.org/10.1016/j.endm.2009.11.027.
  21. Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-SAT. J. Comput. Syst. Sci., 62(2):367-375, 2001. URL: https://doi.org/10.1006/jcss.2000.1727.
  22. Richard M. Karp. Reducibility among combinatorial problems. In Proceedings of a symposium on the Complexity of Computer Computations, held March 20-22, 1972, at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York, USA, pages 85-103, 1972. URL: http://www.cs.berkeley.edu/%7Eluca/cs172/karp.pdf, URL: https://doi.org/10.1007/978-1-4684-2001-2_9.
  23. Lefteris M. Kirousis, Evangelos Kranakis, Danny Krizanc, and Yannis C. Stamatiou. Approximating the unsatisfiability threshold of random formulas. Random Struct. Algorithms, 12(3):253-269, 1998. URL: https://doi.org/10.1002/(SICI)1098-2418(199805)12:3<253::AID-RSA3>3.0.CO;2-U.
  24. Leonid A. Levin. Universal search problems. Problems of Information Transmission, 9(3), 1973. Google Scholar
  25. Andrea Lincoln and Adam Yedidia. Faster random k-cnf satisfiability. arXiv preprint, 2019. URL: http://arxiv.org/abs/1903.10618.
  26. Chao Ming-Te and John Franco. Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k-satisfiability problem. Information Sciences, 51(3):289-314, 1990. Google Scholar
  27. Eugene Nudelman, Kevin Leyton-Brown, Holger H. Hoos, Alex Devkar, and Yoav Shoham. Understanding random SAT: beyond the clauses-to-variables ratio. In Principles and Practice of Constraint Programming - CP 2004, 10th International Conference, CP 2004, Toronto, Canada, September 27 - October 1, 2004, Proceedings, pages 438-452, 2004. URL: https://doi.org/10.1007/978-3-540-30201-8_33.
  28. Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, and Francis Zane. An improved exponential-time algorithm for k-SAT. J. ACM, 52(3):337-364, 2005. URL: https://doi.org/10.1145/1066100.1066101.
  29. Ramamohan Paturi, Pavel Pudlák, and Francis Zane. Satisfiability coding lemma. Chicago J. Theor. Comput. Sci., 1999, 1999. URL: http://cjtcs.cs.uchicago.edu/articles/1999/11/contents.html.
  30. Uwe Schöning. A probabilistic algorithm for k-sat and constraint satisfaction problems. In 40th Annual Symposium on Foundations of Computer Science, FOCS '99, 17-18 October, 1999, New York, NY, USA, pages 410-414, 1999. URL: https://doi.org/10.1109/SFFCS.1999.814612.
  31. Bart Selman, David G. Mitchell, and Hector J. Levesque. Generating hard satisfiability problems. Artificial Intelligence, 81(1):17-29, 1996. Frontiers in Problem Solving: Phase Transitions and Complexity. URL: https://doi.org/10.1016/0004-3702(95)00045-3.
  32. Greg Valiant. Faster random SAT. Personal communication. Google Scholar
  33. Nikhil Vyas and Ryan Williams. On super strong ETH. In Mikolás Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 406-423. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_28.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail