【发布时间】：2020-07-12 23:25:37
【问题描述】：
SAT 求解器可用于解决旅行商问题，其中所选边之间的成本总和很重要。我了解到您随后要求求解器再次寻找较低的成本。该最大值如何以合取范式表示？
【问题讨论】：
-
如果您提供额外的材料，我会帮助您。
标签： sat cnf conjunctive-normal-form
【发布时间】：2020-07-12 23:25:37
【问题描述】：
这个想法是将伪布尔约束转换为 CNF，并且可以使用许多不同的编码。一种朴素的编码是枚举所有会导致更高成本（指数级）的部分模型。
注意：我是以下出版物的合著者： 您可能会发现 PBLib 很有用，因为它提供了不同的编码。
【讨论】：