布尔可满足性 - 算法

Question

我有一个布尔公式：(x_{1} or x_{2}) and (x_{3} or x_{4}) and ..... and (x_{2r-1} or x_{2r})，其中 x_{i} 属于集合：{p_{1}, p_{2}, ... p_{99} , ~ p_{1}, ~p_{2}, ... ~p_{99} } 我必须确定对于 x_{i} 给定公式的某些值是否为真.

我知道它通常在计算上很困难。但是有什么非常快速的方法可以解决这个特殊问题吗？到目前为止，我已经尝试过回溯——即在递归中，我为每个可能的变量替换了每个可能的值（0 或 1，所以不多），并且每个尚未获得值的变量都是微不足道的。在深入递归之前，我会检查公式（即使不是每个变量都有值），如果它是假的，我不会更深入。但它太慢了。有任何想法吗？非常感谢您的帮助。

Answer 1

如果每个 OR 子句只有两个变量，那么您有 2-SAT，它具有线性时间解。