我们知道任何表达式都可以在线性时间内转换为 CNF，其中 CNF 结果与原始表达式“逻辑上等价”，但“可满足性”是不变的，这意味着当且仅当原始表达式为可满足（例如可以通过计算“Tseitin 导数”来完成）。假设可以在多项式时间内检查 CNF 的可满足性，则可以在多项式时间内检查原始表达式的可满足性。因此，可以在多项式时间内检查任何表达式的可满足性。然而，SAT 问题是 NP 完全问题，所以这不是真的。但我哪里出错了？我假设解释来自“CNF 在逻辑上不等于原始表达式”，但话又说回来，这对于检查可满足性并不重要（？）。预先感谢您的帮助。
CNF sat 无法在线性时间内检查。事实上，即使是受限的 3-CNF SAT 也是 NP 完全的。请参阅https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#3-satisfiability。