真值表方法，作为命题逻辑的最简单的语义证明系统，表示可以在有限时间内确定任何公式的每个模型的算法。因此，这些不可满足，可满足且有效的公式是可以确定的。用于满足性的真值表方法的计算时间在最坏情况下随着变量数n呈指数增长，因为真值表具有2 n行。优化（语义树的方法）避免查看子句中不存在的变量，因此在许多情况下节省了计算时间，但在最坏的情况下，它同样是指数的。
在最坏的情况下，派生条款的数量随着初始条款的数量呈指数增长。因此，为了在两个过程之间做出决定，我们可以使用经验法则，在许多变量很少的子句的情况下，真值表方法更可取，并且在很少变量的子句的情况下，分辨率可能会完成快点。
问题仍然存在：命题逻辑中的证据能否更快？有更好的算法吗？答案：可能不是。毕竟，复杂性理论的创始人S.库克已经证明3-SAT问题是NP完全的。3-SAT是所有CNF公式的集合，其子句正好有三个文字。因此很明显，对于3-SAT，可能存在（模P / NP问题）没有多项式算法，因此可能也不是一般算法。然而，对于Horn子句，存在一种算法，其中用于测试可满足性的计算时间仅随着公式中文字数量的增加而线性增长。
意见反馈