Structural Information And Clustering Properties Of CNF Formula Assignment Space

The problem of satisfiability has attracted much attention in many fields of computer science.Combinatorial constraint problems of different forms can be transformed into satisfiability problems in polynomial time.A method widely used to study the problem of satisfiability is to convert it into the form of a factor graph.As a tool of reasoning the marginal probability of variables,factor graph is used in various information transmission algorithms to effectively improve the efficiency of solving the problem of satisfiability.By paying attention to the structural information of variables and clauses on the factor graph,we can explore the satisfiability of the CNF formula,or analyze the potential structural information between clauses and arguments through data mining techniques.Therefore,the structural information implied by CNF formula provides a new method for exploring the problem of satisfiability.In this paper,with the assignment as the node,based on the value of the number of clauses under the control of the flip boundary,a class of directed graphs--BF maps is introduced.It is expected that the relationship between the solutions can be satisfied through the structural information on the BF graph.This paper studies the structural properties and clustering phenomena of the matching formula formula assignment space under satisfying conditions,and provides a new idea for solving the SAT problem.The main findings of this paper are:(1)The probabilistic properties of satisfying solution by random walk on BF graph are given.It is found that for a CNF formula with n variables and m clauses,the probability of obtaining a satisfiable solution on the BF graph increases with the increase of flip control parameter k.What’s more,when the parameter k approaches n,the probability is stable.It proves that for a satisfiable CNF formula,t steps random walks are performed on BF graphs with arbitrary k-values.When t is large enough,the probability of obtaining a satisfiable solution will eventually converge to 1.Finally,experimental simulation supports the correctness of the property(2)The clustering phenomenon is explored by analyzing the satisfiable solutions in the assignment space of the CNF formula.There is a clustering phenomenon in the CNF formula assignment space that satisfies the solution,and the number of solution clusters changes with the change of the constraint density,which is in accordance with the solution space of the symmetry breaking average field theory of the replica in statistical physics.In this paper,by introducing effective part assignment,constrained arguments and other related knowledge discovery: each can satisfy a unique core in the solution,every satisfiable solution belonging to the same cluster has the same core.