A k-CNF(conjunctive normal form)formula is a regular(k,s)-CNF one if every variable occurs s times in the formula,where k≥2 and s>0 are integers.Regular(3,s)-CNF formulas have some good structural properties,so ca...A k-CNF(conjunctive normal form)formula is a regular(k,s)-CNF one if every variable occurs s times in the formula,where k≥2 and s>0 are integers.Regular(3,s)-CNF formulas have some good structural properties,so carry-ing out a probability analysis of the structure for random formulas of this type is easier than conducting such an analysisfor random 3-CNF formulas.Some subclasses of the regular(3,s)-CNF formula have also characteristics of intractabilitythat differ from random 3-CNF formulas.For this purpose,we propose strictly d-regular(k,2s)-CNF formula,which is aregular(k,2s)-CNF formula for which d≥0 is an even num-ber and each literal occurs s-d/2 or s+d/2 times(the literals from a variable x are x and-x,where x is positive and-x isnegative).In this paper,we present a new model to generatestrictly d-regular random(k,2s)-CNF formulas,and focuson the strictly d-regular random(3,2s)-CNF formulas.Let F be a strictly d-regular random(3,2s)-CNF formula suchthat 2s>d.We show that there exists a real number so suchthat the formula F is unsatisfiable with high probability whens>so,and present a numerical solution for the real numberso.The result is supported by simulated experiments,and isconsistent with the existing conclusion for the case of d=0.Furthermore,we have a conjecture:for a given d,the strictlyd-regular random(3,2s)-SAT problem has an SAT-UNSAT(satisfiable-unsatisfiable)phase transition.Our experimentssupport this conjecture.Finally,our experiments also showthat the parameter d is correlated with the intractability of the 3-SAT problem.Therefore,our research maybe helpful for generating random hard instances of the 3-CNF formula.展开更多
基金The authors would like to thank the National Natural Science Foundation of China for supporting this work(Grant Nos.61762019,61462001 and 61862051)thank Haiyue Zhang,and ZufengFu for their suggestions for the article writing.
文摘A k-CNF(conjunctive normal form)formula is a regular(k,s)-CNF one if every variable occurs s times in the formula,where k≥2 and s>0 are integers.Regular(3,s)-CNF formulas have some good structural properties,so carry-ing out a probability analysis of the structure for random formulas of this type is easier than conducting such an analysisfor random 3-CNF formulas.Some subclasses of the regular(3,s)-CNF formula have also characteristics of intractabilitythat differ from random 3-CNF formulas.For this purpose,we propose strictly d-regular(k,2s)-CNF formula,which is aregular(k,2s)-CNF formula for which d≥0 is an even num-ber and each literal occurs s-d/2 or s+d/2 times(the literals from a variable x are x and-x,where x is positive and-x isnegative).In this paper,we present a new model to generatestrictly d-regular random(k,2s)-CNF formulas,and focuson the strictly d-regular random(3,2s)-CNF formulas.Let F be a strictly d-regular random(3,2s)-CNF formula suchthat 2s>d.We show that there exists a real number so suchthat the formula F is unsatisfiable with high probability whens>so,and present a numerical solution for the real numberso.The result is supported by simulated experiments,and isconsistent with the existing conclusion for the case of d=0.Furthermore,we have a conjecture:for a given d,the strictlyd-regular random(3,2s)-SAT problem has an SAT-UNSAT(satisfiable-unsatisfiable)phase transition.Our experimentssupport this conjecture.Finally,our experiments also showthat the parameter d is correlated with the intractability of the 3-SAT problem.Therefore,our research maybe helpful for generating random hard instances of the 3-CNF formula.
