Please consider the following 3-SAT instance and the corresponding graph

enter image description here

The graph can be displayed in other two forms

enter image description here

The Tutte polynomial for this graph is

enter image description here

The independence number of the graph is 4, then the considered 3-SAT instance is satisfiable. This fact is checked using the code:

x1, x2, x3 = Bools('x1 x2 x3')
s=Solver()
s.add(Or(x1,x2,Not(x3)),Or(x1,Not(x2),x3),Or(Not(x1),x2,x3),Or(Not(x1),Not(x2),Not(x3)))
print s
print s.check()
m = s.model()
print m  

and the corresponding output is:

sat
[x3 = False, x2 = False, x1 = False]

The corresponding complement of the graph is

enter image description here

and the Tutte polynomial for the complement of the graph is

enter image description here

The clique number of the complement is 4 and then it says that the considered 3-SAT instance is satisfiable.

The question is : It is possible to use the Tutte polynomial to decide if the considered 3-SAT instance is satisfiable ?

有帮助吗?

解决方案 2

Other example:

enter image description here

The Tutte polynomial is:

enter image description here

The independence number of the graph is 3, then the considered 3-SAT instance is satisfiable. This fact is checked using the code:

x1, x2, x3, x4 = Bools('x1 x2 x3 x4')
s = Solver()
s.add(Or(Not(x1),x2,x3),Or(x1,Not(x2),x3),Or(Not(x1),x2,x4))
print s.check()
m = s.model()
print m

and the corresponding output is:

sat
[x3 = False, x2 = False, x1 = False, x4 = False]

The corresponding complement of the graph is

enter image description here

and the Tutte polynomial for the complement of the graph is

enter image description here

The clique number of the complement is 3 and then it says that the considered 3-SAT instance is satisfiable.

其他提示

Other example:

enter image description here

the graph can be displayed in other two forms:

enter image description here

The Tutte polynomial for this graph is:

enter image description here

The independence number of the graph is 3, then the considered 3-SAT instance is satisfiable. This fact is checked using the code:

x, y, z = Bools('x y z')
s = Solver()
s.add(Or(x,y,z),Or(Not(x),Not(y),Not(z)),Or(x,Not(y),Not(z)))
print s.check()
m = s.model()
print m

and the corresponding output is:

sat
[z = False, y = True, x = False]

The corresponding complement of the graph is

enter image description here

and the Tutte polynomial for the complement of the graph is

enter image description here

The clique number of the complement is 3 and then it says that the considered 3-SAT instance is satisfiable.

The question is : It is possible to use the Tutte polynomial to count the possible models for the considered satisfiable 3-SAT instance?

许可以下: CC-BY-SA归因
不隶属于 StackOverflow
scroll top