将问题转换为 CIRCUIT-SAT

Question

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

Partial Weighted Max SAT 由一组硬分句和一组加权软分句组成。我们寻求一个满足所有硬子句并从软子句中获得至少 k 权重的分配。

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

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

谢谢

Answer 1

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

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

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

• MiniSAT+
• Z3 by Microsoft Research
• ...（在此处查看其他人：https://en.wikipedia.org/wiki/Satisfiability_modulo_theories#SMT_solvers）

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

从 SAT 到 Circuit SAT，您必须使用Tseitin transformation，您的问题将得到解决:)。