0

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

4

1 回答 1

1

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

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

于 2020-07-21T22:30:13.390 回答