A Study On The Satisfiability Of Strictly D-regular Stochastic (3,s)-CNF Formulations

The satisfiability(SAT)problem determines whether a conjunctive normal form(CNF)formula is satisfiable,where a CNF formula is satisfiable means that there exists an assignment a such that the value of the formula is true when its variables are assigned the values σ.The SAT problem universally uses in the fields of artificial intelligence,automated theorem proving,integrated circuit design,computational complexity,and so on.The existing researches show that the random k-SAT problem possesses an SAT-UNSAT phase transition relating to the ratio of the number of clauses to the number of variables.However,the ratio is equal to s/k or a regular(k,s)-CNF formula.Hence the ratio is no longer suitable for studying the regular(k,s)-SAT problem when the parameter s fixes.As a result,we impose a constraint on a regular(k,s)-CNF formula to obtain a strictly d-regular(k,s)-CNF formula.The constraint is that the absolute value of the difference between positive and negative occurrence numbers of every variable in the formula is d.A strictly d-regular(k,s)-CNF formula is a strictly regular(k,s)-CNF formula when d=0.Because the regular(3,s)-SAT problem is NP-complete when 5≥ 4,we mainly study strictly d-regular random(3,s)-CNF formulas.The research includes a generating model,analysis of intractability,satisfiability threshold,and so on.The main work and contributions are as follows.(1)A novel model called SDRRKS is presented,which generates strictly d-regular random(k,s)-CNF formulas.Some experiments were conducted to preliminarily explore the satisfiability and the intractability of strictly d-regular random(3,s)-CNF formulas.The experiments show that under some conditions,the strictly d-regular random(3,s)-SAT problem possesses SAT-UNSAT phase transitions related to s and d,and both s and d affect the intractability of the strictly d-regular random(3,s)-SAT problem.(2)Minimal unsatisfiable formulas are used in polynomial-time reduction to analyze the intractability of the strictly d-regular random(3,s)-SAT problem.The strictly s-regular(3,s)-SAT problem is easy to solve.Let s>4 be an integer,then:either each strictly(s-2)-regular(3,s)-CNF formula is satisfiable or the strictly(s-2)-regular(3,s)-SAT problem is NP-complete;and a similar conclusion holds for the strictly(s-4)-regular(3,s)-SAT problem.The strictly d-regular(3,s)-SAT problem is NP-complete when s≥6 and 0 ≤d ≤s-6 are integers.It needs to say that the conclusions above hold for the strictly d-regular random(3,s)-SAT problem.So studying the strictly d-regular random(3,s)-SAT problem is theoretically meaningful.(3)The first moment method uses to study the satisfiability threshold of strictly d-regular random(3,s)-CNF formulas.If the parameter d>0 fixes,then there exists a real number s0 such that a strictly d-regular random(3,s)-CNF formula is unsatisfiable with high probability when s>s0.If the parameter s≥ 12 fixes,then there exists a real number d0 such that a strictly d-regular random(3,s)-CNF formula is unsatisfiable with high probability when d<d0.Our simulated experiments verify the two conclusions well,and the conclusions support the SAT-UNSAT phase transitions observed experimentally.