3-СБ и Тутте полином

Question

Пожалуйста, рассмотрим следующий 3-SAT экземпляр и соответствующий граф

На графике может отображаться в двух других формах

Татта полином для этого графика равен

Число независимости графика равно 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

Другой пример:

Татта полином:

Число независимости графа равна 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

Другой пример:

график может отображаться в двух других формах:

Татта полином для этого графа:

Число независимости графа равно 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?