Structural Information And Phase Transition Properties Of Balancing Regular (k,2r)-CNF Formula

The Boolean satisfiability problem is the core issue in theoretical computer science.People have been working hard to find the intricate nature of the CNF formula.By defining the structure of the CNF formula,such as the length of the clause,the number of occurrences of Boolean variables,etc.,and based on this,the structural information of the CNF formula is analyzed,and an efficient algorithm is designed.The balancing regular(k,2r)-CNF formula studied in this paper is a kind of CNF formula with regular structure.By defining the length of each clause is k,the number of positive and negative occurrences of each Boolean variable is r.The difficulty of solving the instance is more difficult than the general k-CNF formula.In this paper,we study the balancing regular(k,2r)-CNF formula from the instances of model generation,structure information,solving algorithm and phase transition properties.The main research results are as follows:(1)In order to analyze the structural information and phase transition properties of the balancing regular(k,2r)-CNF formula,a stochastic model-BR(n,k,2r)model for generating the balancing regular(k,2r)-CNF formula is constructed.The model can efficiently generate non-repetitive clauses of balancing regular(k,2r)-CNF formula.(2)The structural information of the balancing regular(k,2r)-CNF formula is studied by expressing the balancing regular(k,2r)-CNF formula as the variable interaction graph and the factor graph.The experiment found that in the variable interaction graph,the degree of the vertex is positively correlated with the clause-variable ratio of the formula;in the factor graph,the clauses and the variables are staggered.(3)Based on the special structural information of the balancing regular(k,2r)-CNF formula,the initial assignment of the Stochastic Local Search(SLS)algorithm is improved to solve the regular formula.The experimental results show that the improved SLS algorithm can solve the balancing regular(k,2r)-CNF formula more effectively than the original algorithm.(4)The instance of balancing regular(k,2r)-CNF formula will have a satisfiability phase transition phenomenon as the clause-variable ratio increases.Through theoretical analysis,an upper bound of the phase transition threshold of the balancing regular(k,2r)-CNF formula is given as 2~k ln 2-kln 2/2and a lower bound is 2~k ln 2-kln 2/2-2 ln 2.