3-飽和和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實例是可滿足的。這一事實被使用的代碼檢查：

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實例是可滿足的。

Answer 2

其它示例：

圖表可顯示在其它兩種形式：

對於該曲線圖的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實例的可能模型？