algorithm - 最小不可满足核心算法
问题描述
我正在寻找一种多项式算法来找到给定 CNF 公式的最小不可满足核心。换句话说，一种算法，如果它输入一个布尔不可满足的 CNF，它会输出给定 CNF 的子句的子集，这样当我们从子集中删除子句时，它们是不可满足的并且变得可满足。如果给定 CNF 是可满足的，则算法返回给定 CNF 的子句的可满足子集。算法复杂度必须是多项式的。
解决方案
鉴于决定 CNF 是可满足还是不可满足是 NP 完全的（除非 P = NP），您将找不到用于此的多项式算法。
推荐阅读
- awk - 删除文本行，直到到达新的空白行
- python - 在字符串中找到左半边的count(symbols)=右半边的count(symbols)的索引？
- css - 将背景图像放在菱形容器中会导致容器失去形状
- javascript - Vue.js 中类似网格的游戏地图的更高效数据
- node.js - 将 Express Routes 与 Google Assistant 意图匹配
- vue.js - Vue.js 中远程图像的 CORS 问题
- html - 使用 CSS Grid 对齐极端的项目
- mongodb - 容器启动时无法初始化 MongoDB
- python - 如何使用函数在python中导入变量？
- html - 浏览器在正文中移动 DOCTYPE 和 head 标签