避免 NP 完全性的受限布尔公式

Question

我有布尔公式 A 和 B，想要检查“A -> B”（A 意味着 B）在多项式时间内是否为真。

对于完全通式 A 和 B，这是 NP 完全的，因为“A -> B”为真”与“not (A -> B)”相同是不可满足的。

我的目标是找到有用的限制，以便可以进行多项式时间验证。我也有兴趣找到 O(n) 或 O(n log n) 限制（n 是某种长度 |A| 或 |B|）。我宁愿限制 B 而不是 A。

一般来说，我知道以下几类“更简单”的布尔公式：

• （可重命名）Horn 公式可以在线性时间内求解（它们是 CNF 形式，最多有一个正变量）。
• DNF形式的所有公式都很容易检查
• 2-SAT 是 CNF 公式，每个子句最多有 2 个变量，可在线性时间内求解。
• XOR-SAT 是用 XOR 而不是 OR 的 CNF 公式。它们可以通过高斯消去法求解，时间复杂度为 O(n^3)

主要问题是我有公式“A -> B”又名“（不是A）或B”，对于非平凡的A/B，它很快就变成非CNF和非DNF。

如果我正确理解了 Tseytin 变换，那么我可以将任何公式 X 转换为 CNF Y，其中 O(|X|) = O(|Y|)，因此我可以假设 - 如果我愿意 - 我的公式是 CNF .

有一些容易实现的目标：

• 如果|B|是常数且很小，我可以枚举 B 的所有解决方案并检查它们是否产生真正的 A。
• 类似地，如果 |A|是常数且很小，我可以枚举 A 的所有解决方案并检查它们是否产生错误的 B

更有趣的是：

• 如果 B 在 DNF 中，那么我可以将 A 转换为 CNF，这将使“（不是 A）或 B”DNF 可以在线性时间内解决。
• 对于一般B，如果|B|是 O(log |A|)，我可以将 B 转换为 DNF 并以这种方式解决它

但是，我不确定如何使用其他更简单的课程，或者是否可能。

由于分布性，当试图将“（不是 A）或 B”带回 CNF 时，CNF 中的 A 或 B 几乎肯定会呈指数级爆炸 - 如果我没记错的话。

注意：我的用例可能有比 B 公式更复杂/更长的 A 公式。

所以我的问题归结为：是否存在有用的布尔公式 A 和 B 类，使得“A -> B”可以在多项式（最好是线性）时间内证明？ - 除了我已经提到的 4 个案例。

编辑：对此的不同看法：在 A 和 B 的什么条件下，在以下类别之一中是“A -> B”：

• 在DNF
• CNF 和 Horn 公式 (Horn-SAT)
• CNF 和二元公式 (2-SAT)
• CNF 和算术公式（XOR 的 CNF）

Answer 1

“对于完全通用的公式 A 和 B，这是 NP 完全的，因为“A -> B”为真”与“not (A -> B)”不可满足。”

不可满足就是不可满足。因此，您解决的问题是共同 NP 完全问题。