将复杂逻辑表达式转换为CNF(无指数放大)

Question

在我的布尔逻辑问题中，我有一组长度超过10,000(从10到100k)的变量(编码为整数)。每个变量都有自己的约束集，即来自同一集合的其他变量与它相矛盾。矛盾是相互的，即

(1 & -2) | (2 & -1)

任务是最大化相互满足的变量的数量。在SAT术语中，应表述为:

MAXIMIZE {
(1 & -2 & -3 ...) |
(2 & -1 & -4 ...) |
...
}

这个表达式直观地是DNF格式，但是SAT求解器使用CNF表达式，因此需要进行转换。

我想:

• 用SAT求解器求解表达式(我使用PySAT工具包)，这意味着将其转换为CNF形式，同时避免子句的指数增长(需要应用tseittin变换/基数约束—但只是不知道如何);
• 最大化表达式中真实子句的数量，即解决一个'max-SAT'问题，具有最大数量的满足变量

请帮助我制定一个有效的CNF(参考如何在Python SAT求解器中完成或只是原始表达式)。

Answer 1

如果我对你的问题理解正确的话，我认为普通的SAT解算器帮不了你。本质上，DNF形式是SAT问题的解决方案:每个子句都简单地进行赋值，使语句为真。你的问题听起来更像是一个"最大集合覆盖"，是的，你可以强迫SAT求解器为你做这个，但这可能不是最简单的方法。(我个人喜欢GNU Mathprog做这样的事情。如果问题太大，那就为Gurobi买单吧。

你考虑过贪婪的方法吗?有一个真正的最大值真的很重要吗?我模模糊糊地记得听说过使用这个公式来找到最大覆盖问题的合适解。