3-cnf-sat 有一个扭曲的问题

Question

如果把3-cnf-sat问题改成如下：
对于每个 c_i，c_i = -x_i1 OR -x_i2 OR x_{i3 表示其中一个变量出现时没有否定。
您还可以为某些（或全部）x 赋予值（0 或 1）。
您应该能够在多项式时间内解决问题（找到满足问题或证明问题不可满足的 x 值）。}

1. 解决此问题的多项式运行时间算法是什么？
2. 证明它在多项式时间内运行。

提示：表明 c_i = -x_i1 OR -x_i2 OR x_i3 等于 c = (x_i1 AND -x_i2) -> x_i3

Answer 1

您描述的公式是霍恩公式的子集。因此，可满足性问题并不比Horn satisfiability 更难，并且承认相同的线性时间解决方案。