java - Alloy 中的 A4options.symmetry 和签名实例排列

Question

我在 Alloy 中建模了一个图表转换链。我对解决结果的任何链都感兴趣，但有些链是完全相同的。除了签名实例之间的排列之外，它们是相同的，但实例之间的关系从一种解决方案到另一种解决方案形成完全相同的图。

有没有办法避免这些冗余的解决方案？我在 A4Option 类中看到了一个对称选项，但我不太明白如何配置它。

    /** This option specifies the amount of symmetry breaking to do (when symmetry breaking isn't explicitly disabled).
 *
 * <p> If a formula is unsatisfiable, then in general, the higher this value,
 * the faster you finish the solving. But if this value is too high, it will instead slow down the solving.
 *
 * <p> If a formula is satisfiable, then in general, the lower this value, the faster you finish the solving.
 * Setting this value to 0 usually gives the fastest solve.
 *
 * <p> Default value is 20.
 */

这是否意味着如果我输入 0 它就会被禁用？如果我设置更高的值，它会避免对称吗？如果将一组原子以及这些原子之间的关系视为一个图。邻接矩阵表征矩阵中原子之间的关系。对称是否意味着 2 个实例具有等效的邻接矩阵？

为了降低求解复杂度，有没有办法向求解器指定我们对某些特定的签名实例排列或关系排列不感兴趣，而是对其架构配置感兴趣？

提前致谢。

Answer 1

Does it mean if I put 0 [symmetry breaking] is disabled?

是的

if I put a higher value does it avoid symmetry?

是的，这是最好的。

Does symmetry means 2 instances that have equivalent adjacency matrix?

我不知道你所说的“邻接矩阵”是什么意思，但无论如何，答案很可能是“不一定”。对称性破缺只是一种启发法；它是在低于合金 AST 的级别实现的，这意味着合金分析器不一定会自动检测和破坏在域模型的高级别上有意义的一些对称性。

In order to reduce the solving complexity, is there a way to specify to the solver that we are not interested in some specific signature instances permutation or relation permutation but in their architecture configuration?

我认为使用 Alloy 不容易做到这一点。