The Critical Phenomenon And Structure Characteristics Of D-Regular(k,s)-SAT

The Satisfiability Problem(SAT)is an important Problem in theoretical computer science.The theoretical analysis and experimental verification of the phase transition phenomenon of random k-SAT problems show that the constraint density is an important parameter that affects the satisfiability of the CNF formula.When the constraint density of a formula is close to the phase transformation point,the SAT problem is difficult to be solved.Otherwise,it is easy to be solved.However,the NP-completeness of regular(k,s)-SAT problem shows that only Using the constraint density to describe the solving difficulty of SAT problem is rough.The SAT problem encoded from a practical problem often has some special structure.It is always a research focus how to use these special structures to quickly solve the practical problems.In order to understand the nature of SAT problem and design a more effective SAT algorithm,we set limits on the absolute value of the difference between positive and negative occurrences of every variable,and introduce the d-regular(k,s)-CNF formula.A d-regular(k,s)-CNF formula is a regular(k,s)-CNF formula,in which the absolute value of the difference between positive and negative occurrences of every variable is at most a nonnegative integer d.The d-regular(k,s)-CNF formula has stronger regular constrains than the(k,s)-CNF formula and the regular(k,s)-CNF formula.Thus,we mainly carry out our research on the structure characteristics of d-regular(k,s)-CNF formula,the critical phenomenons of d-regular(k,s)-SAT problem,the existence condition of uniquely satisfiable d-regular(k,s)-CNF formula and the critical phenomenons of several special(1,0)-SAT problems.Our contributions in this paper are the following:(1)We analyze the structural characteristics of d-regular(k,s)-CNF formula,and study the NP completeness and the critical phenomenon of the d-regular(k,s)-SAT problem.We present a polynomial reduction from a k-CNF formula to a d-regular(k,s)-CNF formula,and prove that for k ?3 the d-regular(k,s)-SAT problem is an NP-complete problem,if there is an unsatisfiable d-regular(k,s)-CNF formula.It reveals that there is a critical function f(k,d)for k ?3 such that every d-regular(k,s)-CNF formula is satisfiable for s ?f(k,d)and the d-regular(k,s)-SAT problem is NP-complete for s(29)f(k,d).That is to say,the d-regular(k,s)-SAT problem has the critical phenomenon from triviality(output the affirmative answer without computation)to NP-completeness.It is not known whether the critical function f(k,d)is computable,but we prove that f(k,d)is an increasing function of k and a decreasing function of d.By means of a improved finite non-increasing sequence of positive integers,the upper bound of f(k,d)is obtained for small k.(2)We investigate Uniquely satisfiable d-regular(k,s)-SAT problem.Uniquely satisfiable k-SAT problem is proved to be as difficult to solve as the general k-SAT.We present a method to construct an uniquely satisfiable d-regular(k,s)-CNF formula,and show the existence condition of an uniquely satisfying d-regular(k,s)-CNF formula.Especially,for k ?7,if s ?f(k,d)(10)1,then there is an Uniquely satisfiable d-regular(k,s)-CNF formula.For k ?3,s ?f(k,d)(10)1 and(s(10)d)/ 2(29)k-1,we also present a parsimonious reduction method from k-SAT problem to d-regular(k,s)-SAT problem that ensures the same number of solutions of the two formulas.The reduction method transforms any one k-CNF formula to a SAT-equivalent d-regular(k,s)-CNF formula by adding a large number of new variables and new clauses,but does not change the number of solutions.Although the number of solutions does not be changed,the solution space is obviously expanded and the clause constraint density is adjusted to s/ k.This illustrates that the solutions of the formula are diluted to make it difficult to be solved.This also shows that it is not enough to describe structural features of the CNF formula merely by the constraint density ?.(3)We study the critical phenomenon of several special(1,0)-SAT problems.A(1,0)-super solution is a satisfying assignment such that if the value of any one variable is flipped to the opposite value,the new assignment is still a satisfying assignment.In other words,a(1,0)-super solution of a CNF formula must satisfy at least two liters of every clause.The decision problem whether a CNF formulas has a(1,0)-super solution is denoted as(1,0)-SAT.We analyze the structural characteristics of(k,s)-CNF formula,regular(k,s)-CNF formula and d-regular(k,s)-CNF formula,and obtain some conclusions about theexistence of(1,0)-super solution.By designing some polynomial time reduction methods,it is proved that for k(29)3,(1,0)-(k,s)-SAT problem and(1,0)-regular(k,s)-SAT problem have the critical phenomenon and their critical functions are the same.We also prove that for k(29)4,(1,0)-d-regular(k,s)-SAT problem has the critical phenomenon.Using the structural characteristics of these special formulas,we further show some properties of the critical functions.