用于避免 NP 完备性的受限布尔公式

问：

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

对于完全通用的公式 A 和 B，这是 NP 完全的，因为“A -> B”为真“与”不（A -> B）“相同。

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

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

• （可重命名）喇叭公式可以在线性时间内求解（它们采用 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|），因此，如果我愿意，我可以假设我在 CNF 中有我的公式。

有一些唾手可得的果实：

• 如果 |乙|是常数和小的，我可以枚举 B 的所有解决方案并检查它们是否产生真正的 A。
• 同样，如果 |答|是常数和小的，我可以枚举 A 的所有解并检查它们是否产生假 B

更有趣的是：

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

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

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

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

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

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

• 在DNF中
• CNF 和 Horn 公式 （Horn-SAT）
• 在 CNF 和二进制公式 （2-SAT） 中
• 在 CNF 和算术公式（异或的 CNF）中