computer-science - 3-cnf-sat有一个问题

Question

如果按以下方式更改3-cnf-sat问题:
对于每个ci，ci = -xi1 OR -xi2 OR xi3意味着恰好出现一个变量而没有取反。
还为某些(或全部)x赋予了值(0或1)。
您应该能够在多项式时间内解决问题(找到满足问题的x的值或证明它不满足要求)。

什么是可以解决此问题的多项式运行时间算法？

证明它在多项式时间内运行。

提示:表明ci = -xi1 OR -xi2 OR xi3等于c =(xi1 AND -xi2)-> xi3

Answer 1

您描述的公式是Horn公式的子集。因此，可满足性问题并不比Horn satisfiability难，并且接受相同的线性时间解。