假设您有一个 CNF 公式，其中一些变量标记为特殊。
有没有办法让 SAT Solver（比如 minisat）找到一个解决方案，最大化分配给 true 的特殊变量的数量？
问问题
492 次
3 回答
3
你（我）想要的叫做 Partial Max Sat。有一个名为 qmaxsat 的求解器，它似乎工作得很好。
于 2013-01-31T22:45:47.190 回答
0
不确定是否所有这些都可以处理特殊变量的指示，但至少维基百科为搜索提供了一些方向：
有几个求解器提交到最后的 Max-SAT 评估：
- 基于分支定界：Clone、MaxSatz（基于 Satz）、IncMaxSatz、IUT_MaxSatz、WBO。
- 基于可满足性：SAT4J、QMaxSat。
- 基于不可满足性：msuncore、WPM1、PM2。
检查所有这些的描述应该是可管理的。
于 2013-02-07T12:44:51.663 回答
0
您可以使用 PBC 求解器，例如 minisat+ http://minisat.se/MiniSat+.html 他们使用称为伪布尔约束的附加约束来求解常规 CNF 文件 Minisat+ 还支持此类约束的优化，据我了解，它可以解决您的问题
让 x1, .... xn 是你想要最大化的变量 o 真值分配然后你可以定义约束最大化 +1 x1 ..... +1 xn minisat+ 解决了这样的优化问题
于 2014-02-26T12:48:03.310 回答