Я смоделировал цепочку преобразования диаграммы в 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 экземпляра с эквивалентной матрицей смежности?
Чтобы уменьшить сложность решения, есть ли способ указать решателю, что нас интересует не какая-то конкретная перестановка экземпляров подписи или перестановка отношений, а конфигурация их архитектуры?
Заранее спасибо.
