graph-theory - 3-sat 和 Tutte 多项式

Question

请考虑以下 3-SAT 实例和相应的图表

图表可以用其他两种形式显示

该图的 Tutte 多项式为

图的独立数为 4，则考虑的 3-SAT 实例是可满足的。使用以下代码检查这一事实：

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  

相应的输出是：

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

图的对应补码是

并且图的补码的 Tutte 多项式是

补集的团数是 4，然后它表示所考虑的 3-SAT 实例是可满足的。

问题是：是否可以使用 Tutte 多项式来确定所考虑的 3-SAT 实例是否可满足？

Answer 1

其他示例：

图表可以以其他两种形式显示：

该图的 Tutte 多项式为：

图的独立数为 3，则考虑的 3-SAT 实例是可满足的。使用以下代码检查这一事实：

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

相应的输出是：

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

图的对应补码是

并且图的补码的 Tutte 多项式是

补集的团数是 3，然后它表示所考虑的 3-SAT 实例是可满足的。

问题是：是否可以使用 Tutte 多项式来计算考虑的可满足 3-SAT 实例的可能模型？

Answer 2

其他示例：

Tutte 多项式为：

图的独立数为 3，则考虑的 3-SAT 实例是可满足的。使用以下代码检查这一事实：

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

相应的输出是：

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

图的对应补码是

并且图的补码的 Tutte 多项式是

补集的团数是 3，然后它表示所考虑的 3-SAT 实例是可满足的。