Tree Decomposition Algorithm And Application For The SAT

A tree decomposition of the graph G =(V,E)refers to taking a subset of the node set V as a node of the tree T to make the intersection of the two endpoints on any one of the paths on T included in any of the nodes on the path.The width of the decomposition tree is defined by the number of elements of the minimum(node)corresponding subset on T minus 1;while the tree width of the graph G refers to the smallest width among all decomposition trees.The CNF formula F can be represented by a bipartite graph G =(V èC,E)(factor graph of the formula),where the variable node set V corresponds to the variable set,and the clause node set C corresponds to the clause set in the formula F.The positive(negative)occurrence of the element in the clause is represented by the real(virtual)side.In order to realize the bipartite graph,this paper ignores the symbols on the edges of the formula factor graph.In practical applications,many difficult problems can be solved effectively through limiting the small tree width,and can even be worked out in polynomial time.This paper introduces an algorithm of bipartite graph based on the general tree decomposition algorithm,exploring the relationship between the tree width of the formula factor graph and the difficulty of the solution through experiments.Furthermore,this paper aims to explore a linear CNF formula and its corresponding bipartite graph through the tree decomposition algorithm,which shows that the linear CNF formula has a good upper bound on tree width.And the main research results are as follows:First,a tree decomposition algorithm suitable for bipartite graphs is proposed and applied to the CNF formula instance set based on the tree decomposition algorithm of general undirected graphs,which aims to further explore the structural features of difficult examples in the SAT problem.Through experiments,it turns out that with the increase of the constraint density of the formula clause,the tree width of the formula factor graph is much smaller than the scale of the variable,which lays an experimental foundation for further exploration of difficult examples.At the same time,three classic tree decomposition algorithms are introduced in the paper,and the experimental comparison proves that the tree decomposition algorithm this paper proposed can solve the better tree width.Second,the tree decomposition and tree width of the linear bipartite graph are analyzed through experimental research based on the linear CNF formula class,and the structural characteristics of the CNF formula class are further explored under the condition of small tree width.Studies have shown that the upper bound of the tree width of linear CNF formulas is closely related to the nature of the formula itself.That is,when the number of common variables between any two clauses in the formula is less than or equal to 1,the tree width of the linear CNF formula class is less than or equal to the maximum number of occurrences of the variable in the formula.At the same time,the experimental results show that the upper bound of the tree width of the linear CNF formula is less than or equal to the upper bound of the tree width of the non-linear CNF formula.