Other example:
The Tutte polynomial is:
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
and the Tutte polynomial for the complement of the graph is
The clique number of the complement is 3 and then it says that the considered 3-SAT instance is satisfiable.