3-CNF-飽和與扭曲問題

Question

如果你改變了3-CNF-SAT問題如下：
對於每個C _我，C _我 = -x _I1或-X _I2 OR x _i3這意味着恰好有一個變量出現而沒有否定。
你也給了一些（或全部）x的值（0或1）。
您應該能夠在多項式時間內解決問題（找到滿足問題的x值或證明它不可滿足的值）。

1. 什麼是解決此問題的多項式運行時算法？
2. 證明它運行在多項式時間。

暗示：表明是c _我 = -x _I1或-X _I2或X _I3等於C =（X _I1和-X _I2） - > x _i3

Answer 1

您描述的公式是Horn公式的子集。因此可滿足性問題並不比Horn satisfiability難，並且承認相同的線性時間解決方案。