Experimental observation of the SAT-UNSAT phase transition of the random 3-SAT problem from its model perspective

Graphical abstract

References

[1] Schreiber D, Sanders P . MallobSat: scalable SAT solving by clause sharing. Journal of Artificial Intelligence Research, 2024, 80: 1437–1495

[2] Cook S A. The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. 1971, 151−158

[3] Aspvall B, Plass M F, Tarjan R E . A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Information Processing Letters, 1979, 8( 3): 121–123

[4] Mitchell D, Selman B, Levesque H. Hard and easy distributions of SAT problems. In: Proceedings of the 10th National Conference on Artificial Intelligence. 1992, 459−465

[5] Kaporis A C, Kirousis L M, Lalas E G . The probabilistic analysis of a greedy satisfiability algorithm. Random Structures & Algorithms, 2006, 28( 4): 444–480

[6] Díaz J, Kirousis L, Mitsche D, Pérez-Giménez X. On the satisfiability threshold of formulas with three literals per clause. Theoretical Computer Science, 2009, 410(30−32): 2920−2934

[7] Friedgut E, Bourgain J . Sharp thresholds of graph properties, and the k-SAT problem. Journal of the American Mathematical Society, 1999, 12( 4): 1017–1054

[8] Braunstein A, Mézard M, Zecchina R . Survey propagation: an algorithm for satisfiability. Random Structures & Algorithms, 2005, 27( 2): 201–226

[9] Mézard M, Zecchina R . Random k-satisfiability problem: from an analytic solution to an efficient algorithm. Physical Review E, 2002, 66: 056126

[10] Biere A, Fazekas K, Fleury M, Heisinger M. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020. In: Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions. 2020, 50−53

RIGHTS & PERMISSIONS

The Author(s) 2025. This article is published with open access at link.springer.com and journal.hep.com.cn