如何解决最小不可满足核心算法
我正在寻找一种多项式算法来找到给定 CNF 公式的 minimal unsatisfiable core。换句话说，一种算法，如果它输入一个布尔不可满足的 CNF，它会输出给定 CNF 的子句的子集，这样当我们从子集中删除子句时，它们是不可满足的并变为可满足的。如果给定的 CNF 是可满足的，则算法返回给定 CNF 的子句的可满足子集。算法复杂度必须是多项式的。
解决方法
鉴于决定 CNF 是可满足还是不可满足是 NP 完全的（除非 P=NP），您将找不到用于此的多项式算法。
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
