합금 및 코닥 (Kodkod)의 전체 주문 순서 최적화

Question

분석의 효율성을 높이기 위해 총 주문 관계가 고정되어 있으며 ("012"에서 나타나는 원자 이름을 얻으려면 여러 곳에서 (예 : 여기 enter link description here 또는 there) 자연 "질서).

내가 이해하는 한, 최적화는 Kodkod (in this piece of code)에서 이루어집니다. 그러나 Java 문서보다 부울 행렬에 대해 설명하고 알고리즘에 대한 논증을 제공하지는 않습니다 (소스 코드 문서에서는 문제가 없습니다). 코닥? 내가 말할 수있는 한, E. Torlak의 PhD 논문은 이러한 것들에 대해 언급하지 않았다. (I Shlyakhter의 논문은 다른 최적화에 대해 말하지만, 그것들이 Kodkod 또는 Alloy에서 구현되는지는 모르겠다.)

Answer 1

이 최적화는 찾은 코드 위치의 Kodkod에서 이루어집니다. 이것은 Ilya Shlyakhter's PhD thesis (p. 111, Section 4.5.5)에서 간략하게 설명됩니다.