我有布尔公式 A 和 B 并想检查“A -> B”（A 暗示 B）在多项式时间内是否为真。
对于完全通用的公式 A 和 B，这是 NP 完全的，因为““A -> B”为真”与“非 (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 转换，那么我可以使用 O(|X|) = O(|Y|) 将任何公式 X 转换为 CNF Y，因此我可以假设 - 如果我愿意 - 我在 CNF 中有我的公式。
有一些唾手可得的果实：
- 如果 |B| 是恒定且小的，我可以枚举 B 的所有解决方案并检查它们是否产生真正的 A。
- 同样，如果 |A| 是常数且很小，我可以枚举 A 的所有解决方案并检查它们是否产生错误的 B
更有趣的是：
- 如果 B 在 DNF 中，那么我可以将 A 转换为 CNF，这将使“（不是 A）或 B”DNF 可以在线性时间内求解。
- 对于一般 B，如果 |B| 在 O(log |A|) 中，我可以将 B 转换为 DNF 并以这种方式解决
但是，我不确定如何使用其他更简单的类，或者是否可能。
由于分布性，CNF 中的 A 或 B 几乎肯定会在试图将“（不是 A）或 B”带回 CNF 时呈指数级增长——如果我没记错的话。
注意：我的用例可能比 B 公式更复杂/更长。
所以我的问题归结为：是否存在有用的布尔公式 A 和 B 类别，使得“A -> B”可以在多项式（最好是线性）时间内得到证明？- 除了我已经提到的 4 个案例。
编辑：对此有不同的看法：在以下类别之一中，A 和 B 在什么条件下是“A -> B”：
- 在 DNF
- 在 CNF 和 Horn 公式 (Horn-SAT) 中
- 在 CNF 和二元公式 (2-SAT) 中
- 在 CNF 和一个算术公式（XOR 的 CNF）中