问题描述
我正在寻找一种多项式算法来找到给定 CNF 公式的 minimal unsatisfiable core。换句话说，一种算法，如果它输入一个布尔不可满足的 CNF，它会输出给定 CNF 的子句的子集，这样当我们从子集中删除子句时，它们是不可满足的并变为可满足的。如果给定的 CNF 是可满足的，则算法返回给定 CNF 的子句的可满足子集。算法复杂度必须是多项式的。
解决方法
鉴于决定 CNF 是可满足还是不可满足是 NP 完全的（除非 P=NP），您将找不到用于此的多项式算法。
我正在寻找一种多项式算法来找到给定 CNF 公式的 minimal unsatisfiable core。换句话说，一种算法，如果它输入一个布尔不可满足的 CNF，它会输出给定 CNF 的子句的子集，这样当我们从子集中删除子句时，它们是不可满足的并变为可满足的。如果给定的 CNF 是可满足的，则算法返回给定 CNF 的子句的可满足子集。算法复杂度必须是多项式的。
鉴于决定 CNF 是可满足还是不可满足是 NP 完全的（除非 P=NP），您将找不到用于此的多项式算法。