SAT 求解优化

Question

假设您有一个 CNF 公式，其中包含一些标记为特殊的变量。
有没有办法让SAT求解器（比如minisat）找到一个解决方案，最大化分配给true的特殊变量的数量？

Answer 1

你（I）想要的叫做Partial Max Sat。 有一个名为qmaxsat的求解器，它似乎工作得很好。

Answer 2

不确定所有这些是否可以处理特殊变量的指示，但至少维基百科为搜索提供了一些方向：

有几个求解器提交给了上一次 Max-SAT 评估：

基于
• 分支和绑定：Clone，MaxSatz（基于Satz），IncMaxSatz，IUT_MaxSatz，WBO。
• 基于满足性：SAT4J，QMaxSat。
• 基于不满意性：msuncore，WPM1，PM2。

检查所有这些的描述应该是可管理的。

Answer 3

您可以使用

PBC 求解器，例如 minisat+ http://minisat.se/MiniSat+.html它们使用称为伪布尔约束的附加约束求解常规 CNF 文件Minisat+还支持优化此类约束据我了解，它可以解决您的问题

让 x1， ....xn 是要最大化 o 真值分配数的变量然后，您可以定义约束最大化 +1 x1 ..... +1 xnMiniSat+解决了这样的优化问题