graph-theory - 3-sat およびトゥッテ多項式

Question

次の 3-SAT インスタンスと対応するグラフを検討してください。

グラフは他の2つの形式で表示できます

このグラフのトゥッテ多項式は

グラフの独立数が 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]

対応するグラフの補数は

グラフの補数のトゥッテ多項式は

補数のクリーク数は 4 であり、考慮されている 3-SAT インスタンスは充足可能であると言えます。

問題は次のとおりです。トゥッテ多項式を使用して、考慮されている 3-SAT インスタンスが充足可能かどうかを判断できますか?

Answer 1

その他の例:

グラフは他の 2 つの形式で表示できます。

このグラフのトゥッテ多項式は次のとおりです。

グラフの独立数が 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]

対応するグラフの補数は

グラフの補数のトゥッテ多項式は

補数のクリーク数は 3 であり、考慮されている 3-SAT インスタンスは充足可能であると言えます。

問題は次のとおりです。トゥッテ多項式を使用して、考慮される充足可能な 3-SAT インスタンスの可能なモデルを数えることは可能ですか?