【发布时间】：2022-01-17 18:41:14
【问题描述】：
考虑一些节点之间有一些连接。
我的模型的任务是为节点着色。其中一个条件是黑色节点形成一个全连接集。
如何编码？
注意：以防万一：符号之间的联系是先决条件。
【问题讨论】：
【发布时间】：2022-01-17 18:41:14
【问题描述】：
你试过什么？如果您展示了您尝试过的内容以及卡在哪里，则堆栈溢出效果最好。根据您对图表的建模方式，可能有许多不同的方法。
这里有一个提示可以帮助您入门：在使用 z3 进行编程时，您通常会编写“检查”节点是否完全连接的代码。然后，通过约束求解的魔力，使求解器提供满足该标准的模型。因此，从对图形建模开始，以及如何检查相同颜色的节点是否已连接。
请注意，图形着色、团查找、同构等难题在这个领域也很困难。它们可能更容易编码，但你不应该期望平均性能比穷举搜索大实例更好；除非您的图表具有求解器可以利用的特殊结构。但在这种情况下，您最好还是使用自定义算法，而不是依赖通用 SMT 求解器。当然，这一切都取决于您的主要目标是什么。最好尝试多种方法并选择效果最好的一种。
【讨论】：