【发布时间】：2021-04-08 14:59:13
【问题描述】：
我正在寻找一种多项式算法来查找给定 CNF 公式的minimal unsatisfiable core。换句话说，一种算法，如果它输入一个布尔不可满足的 CNF，它会输出给定 CNF 的子句的子集，这样当我们从子集中删除子句时，它们是不可满足的并且变得可满足。如果给定 CNF 是可满足的，则算法返回给定 CNF 的子句的可满足子集。算法复杂度必须是多项式的。
【问题讨论】：
【发布时间】：2021-04-08 14:59:13
【问题描述】：
鉴于决定一个 CNF 是可满足还是不可满足是 NP 完全的（除非 P=NP），您不会为此找到多项式算法。
【讨论】：
-
我正在寻找的算法不决定给定的 CNF F 是可满足还是不可满足，实际上它输出一个子集 S给定的子句，如果 F 是可满足的，S 是可满足的；如果 F 不可满足 S 是最小不可满足。因此算法的输出是一个 CNF，但我们不知道它是否可以满足。