A Study On The Phase Transition Of The Random Regular SAT Problem

Constraint satisfiability problem(CSP)is a hot issue in theoretical computer science.The satisfiability(SAT)problem of propositional formula is the most classical CSP.k-SAT problem is a particular SAT problem by prescribed the length of each clause to be k for SAT problem,which was shown to be NP –Complete for any k ?3.Random regular(k,r)-SAT problem represents a class of satisfiability problems by prescribed the number of each variable be r for k-SAT problem.The constraint density ? is a control parameter that measures the satisfiability phase transition of the k-CNF formula F.However,constraint density ? is constant for random regular(k,r)-SAT problem.So using the constraint density to measure phase transition phenomenon of random regular(k,r)-SAT problem is invalid.Therefore,it is necessary to discover a new control parameter to measure satisfiability phase transition phenomenon of random regular(k,r)-SAT problem.This research on the phase transition phenomenon and mechanism of random regular(k,r)-SAT problem is good for design efficient algorithm.We mainly carry out our research on the satisfiability phase transition phenomenon of random regular(k,r)-SAT problem.A random instance generation model was introduced to analyze the satisfiability phase transition phenomenon using first moment and second moment methods.The main work and contributions are as follows:(1)A novel model is presented,which generates the random regular(k,3r)-CNF formula.We use the first moment method to estimate the upper bound of the satisfiability threshold,and use the second moment method to estimate the lower bound of the satisfiability threshold for the random regular 1-exact(k,3r)-SAT problem.Numerical experiments are performed on the randomly generated example.The results show that the theoretical results are consistent with the experimental results.(2)We study the restricted occurrence times for literals in random regular SAT problems.In particular,we propose a random regular 2-exact(k,r)-SAT problems and its instances generating model.We use the first moment method to estimate the upper bound of the satisfiability threshold.Numerical experiments are performed on the randomly generated example.The results show that the theoretical results are consistent with the experimental results.