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

Чтобы уменьшить сложность решения, существует ли способ указать решателю, что нас не интересует перестановка некоторых подстановок или перестановка отношений, но в их конфигурации архитектуры?

Заранее спасибо.

Answer 1

Означает ли это, если я положил 0 [нарушение симметрии] отключен?

Да

если я ставлю более высокое значение это избежать симметрии?

Да, самое лучшее, что может.

Имеет ли симметрия 2 экземпляра, которые имеют эквивалентную матрицу смежности?

Я не знаю, что вы подразумеваете под «матрицей смежности», но в любом случае ответ скорее всего «не обязательно». Нарушение симметрии - это всего лишь эвристика; он реализуется на уровне ниже, чем сплав AST, что означает, что некоторые симметрии, которые имеют смысл на высоком уровне вашей модели домена, не обязательно автоматически обнаруживаются и ломаются с помощью анализатора сплавов.

Для того, чтобы уменьшить сложность Решая, есть способ указать к решателя, что мы не заинтересованы в какой-то конкретной подписи экземпляров перестановку или отношения перестановки, но в их конфигурации архитектуры?

Не думаю, что с легкостью можно использовать сплав.