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难，并且承认相同的线性时间解决方案。