sat - 将问题转换为 CIRCUIT-SAT

Question

我有兴趣将部分加权最大 SAT 转换为 SAT。我被建议通过 CIRCUIT SAT。

部分加权最大 SAT 由一组硬条款和一组加权软条款组成。我们寻求一个满足所有硬条款并从软条款中获得至少 k 权重的分配。

我如何将其编码为布尔组合电路？

我可以看到如何轻松地对硬子句进行编码。但是我将如何对软子句进行编码，并将权重与它们相关联，并确保通过令人满意的分配获得至少 k 的权重？

谢谢

Answer 1

您需要将 Partial Weighted Max SAT 编码为伪布尔问题。

只需将硬条款视为具有高权重的加权条款并调整目标值（总和）。

要将其编码为 SAT 公式，您可以使用嵌入在SMT求解器中的技术，例如：

• 迷你SAT+
• 微软研究院的 Z3
• ...（在此处查看其他内容：https ://en.wikipedia.org/wiki/Satisfiability_modulo_theories#SMT_solvers ）

要了解如何，这里有一篇来自 MiniSAT+ 的创建者的文章（ Translating Pseudo-Boolean Constraints into SAT ），他将帮助您理解。

从 SAT 到 Circuit SAT，您将不得不使用Tseitin 转换，您的问题将得到解决:)。