computer-science - 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

您描述的公式是霍恩公式的子集。因此，可满足性问题并不比霍恩可满足性问题更难，并且允许相同的线性时间解。