sat - SAT求解器中的目标函数是如何表示的？

Question

SAT 求解器可用于解决旅行商问题，其中所选边之间的成本总和很重要。我了解到您随后要求求解器再次寻找较低的成本。该最大值如何以合取范式表示？

Answer 1

这个想法是将伪布尔约束转换为 CNF，并且可以使用许多不同的编码。一种简单的编码是枚举所有会导致更高成本（指数级）的部分模型。

注意：我是以下出版物的合著者：您可能会发现PBLib很有用，因为它提供了不同的编码。