3-cnf-sat 带有扭曲问题

Question

如果将3-cnf-sat问题改成如下：
对于每个 c_i，c_i = -x_i1 OR -x_i2 OR x_{i3< /sub> 意味着其中一个变量出现而没有否定。
您还可以为某些（或全部）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 可满足性 更难，并且允许相同的线性时间解决方案。