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

Graphical abstract

1 Introduction

The satisfiability (SAT) problem is an essential building block at the core of automated reasoning, symbolic AI, and formal verification [1]. However, the SAT problem is NP-complete (non-deterministic polynomial-time complete) [2]. Hence, studying the SAT problem has both practical and theoretical significance.

A conjunctive normal form (CNF) formula is a k-CNF formula if every clause contains k literals. The k-SAT problem is a subproblem of the SAT problem limited to processing k-CNF formulas. The k-SAT problem has a linear-time algorithm when k=2 [3], but is NP-complete when k\ge 3 [2]. The criticality enables the 3-SAT problem to attract the attention of many scholars (for example, the scholars of papers [4–6]).

Mitchell et al. [4] presented the random 3-SAT model. A formula generated by the random 3-SAT model is called a random 3-CNF formula. The random 3-SAT problem is also a subproblem of the SAT problem, limited to processing random 3-CNF formulas. The random 3-SAT problem exhibits a SAT-UNSAT (satisfiable-unsatisfiable) phase transition. For a random 3-CNF formula with N variables and M clauses, there exists a function {\alpha }_3(N) such that the formula is satisfiable with high probability when and N is large enough, and that the formula is unsatisfiable with high probability when \frac{M}{N}>{\alpha }_3(N) and N is large enough [7]. From experimental observations, the function {\alpha }_3(N) is supposed to converge to around 4.27 when N is large enough [4,8]. However, existing studies only show 3.52\le {\alpha }_3(N)\le 4.4898 [5,6], and a non-strict method suggests that {\alpha }_3(N) is supposed to converge to 4.267 when N is large enough [9]. In other words, whether the function {\alpha }_3(N) converges to a fixed value when N is large enough is an open problem.

Use the random 3-SAT model to generate some formulas with N variables and M clauses, and compute the ratio of the satisfiable formulas in the generated formulas. If the ratio is close to 1, one has \frac{M}{N}\le {\alpha }_3(N) when N is sufficiently large, owing to the proof by contradiction, and similarly, if the ratio is close to 0, one has {\alpha }_3(N)\le \frac{M}{N}. The predetermined values of N and M cause the above method for observing the SAT-UNSAT phase transition of the random 3-SAT problem (as used in paper [4] etc.) to be limited by the flexibility of the \frac{M}{N} value.

Each clause of a random 3-CNF formula with N variables is generated by randomly choosing a set of 3 variables from the set of N variables and negating each with probability 0.5 [4]. Hence, repeating the above process of generating clauses M times produces a random 3-CNF formula with N variables and M clauses. For every integer 1\le i\le M, let F_i be the formula obtained after the ith above repetition (In this paper, the symbol F_i represents such a formula). If M is large enough, there may be an integer such that F_{i_0-1} is satisfiable and F_{i_0} is unsatisfiable. Fortunately, we have experimentally confirmed this possibility. Since F_{i_0-1} is satisfiable and F_{i_0} is unsatisfiable, for every integer 1\le i\le i_0-1 and every integer i_0\le j\le M, F_i is satisfiable, and F_j is unsatisfiable. Because of the possible relation between this fact and the SAT-UNSAT phase transition of the random 3-SAT problem, we generate random 3-CNF formulas with the same feature as F_{i_0} to experimentally observe the SAT-UNSAT phase transition of the random 3-SAT problem (The rationality of this method refers to Section 3).

2 Method

Let F be an unsatisfiable random 3-CNF formula. Since a CNF formula with one clause is satisfiable, there is an integer i_0>1 such that F_{i_0-1} is satisfiable and that F_{i_0} is unsatisfiable. Hence, we use Algorithm 1 to generate the formulas we look forward to.

For every N\in \{170,220,270,320,370\} (Our experiments are very time-consuming when N equals 420) and every \alpha \in \{5.0,5.4,5.8\} (Our tentative experiments show that \alpha affects the experimental results and that Algorithm 1 may not output formula F_{i_0} when \alpha is less than 5.0), we ran Algorithm 1 100 times (Our tentative experiments show that the number is sufficient) to conduct our experiments. We use the Kissat solver [10] to determine whether a CNF formula is satisfiable in the experiments.

3 Results and discussion

Let F_{i_0} be the formula generated by Algorithm 1. Suppose that F_{i_0} has M_{i_0} clauses so that F_{i_0-1} has M_{i_0}-1 clauses. Since our experiments show that generating F_{i_0} is a high-probability event, one has \frac{M_{i_0}-1}{N}\le {\alpha }_3(N)\le \frac{M_{i_0}}{N} when N is sufficiently large, owing to the proof by contradiction. Hence, we present the experimental results in the manner shown in Table 1.

Fit \frac{M_{i_0}}{N}=a+\frac{b}{N} from the data in Table 1 to get \frac{M_{i_0}}{N}\approx 4.249732+\frac{10.875156}{N}, where the goodness of the fit equals 0.404972 (Due to limited data volume, it is not ideal to fit with a degree higher than one). So, {\alpha }_3(N) should converge to 4.249732 when N is large enough. Our observation method eliminates the restriction on the flexibility of the parameter value in the existing observation method.

4 Conclusions

This paper generated a novel class of random 3-CNF formulas to experimentally observe the SAT-UNSAT phase transition of the random 3-SAT problem. The observation method differs from the existing one and eliminates the restriction on the flexibility of the parameter value in the existing one. Thus, our work should be a novel attempt to study the SAT-UNSAT phase transition of the random 3-SAT problem.

It is necessary to increase the number of variables for further experimental observation in the next step. Of course, exploring the structural characteristics of such formulas to support algorithm design for the random 3-SAT problem should also be worth trying.

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