Pergunta

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 ?

Foi útil?

Solução 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.

Outras dicas

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?

Licenciado em: CC-BY-SA com atribuição
Não afiliado a StackOverflow
scroll top