The phase transition in random regular exact (3 s + s , k )-SAT problem
Ao Tang, Xiaofeng Wang, Qingyuan Peng, Junxia Wang, Yi Yang, Fei He, Yingying Hua · Journal of Intelligent & Fuzzy Systems · 2024
A CNF formula with each clause of length k and each variable occurring 4 s times, where positive occurrences are 3 s and negative occurrences are s , is a regular (3 s + s , k )-CNF formula ( F 3 s + s , k formula). The random regular exact (3 s + s , k )-SAT problem is whether there exists a set of Boolean variable assignments such that exactly one literal is true for each clause in the F 3 s + s , k formula. By introducing a random instance generation model, the satisfiability phase transition of the solution is analyzed by using the first moment method, the second moment method, and the small subgraph conditioning method, which gives the phase transition point s* of the random regular exact (3 s + s , k )-SAT problem for k ≥3. When s s* , F 3 s + s , k formula is unsatisfiable with high probability. Finally, through the experimental verification, the results show that the theoretical proofs are consistent with the experimental results.