A4options.symmetry与合金中的签名实例置换

Question

我在“合金”中建立了一个图表转换链。我对求解结果的任何链都感兴趣，但有些链子完全相同。除了签名实例之间的排列外，它们是相同的，但是实例之间的关系构成了从一个解到另一个解的完全相同的图。

有没有办法避免这些多余的解决方案？我在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，它是禁用的？如果我把一个更高的价值，它是否避免对称？如果你把一组原子和这些原子之间的关系当作一个图。一个邻接矩阵作为矩阵中原子之间关系的表征。对称性是否意味着两个具有等价邻接矩阵的实例？

为了降低求解的复杂性，是否有一种方法向求解者说明我们对某些特定的签名实例置换或关系置换感兴趣，而对它们的体系结构配置感兴趣？

提前谢谢。

Answer 1

这是否意味着，如果我把0，对称打破是禁用的？

是

如果我把一个更高的价值，它是否避免对称？

是的，尽力而为。

对称性是否意味着两个具有等价邻接矩阵的实例？

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

为了降低求解的复杂性，是否有一种方法向求解者说明我们对某些特定的签名实例置换或关系置换感兴趣，而对它们的体系结构配置感兴趣？

我不认为使用合金可以轻易做到这一点。