Alloyで次数が一定のグラフを探す

ソフトウェアの抽象モデリングとは、なーんか趣旨と方向性が違うんですが、Alloyを“有限構造の検索装置”として使って遊んでます。

エイトクイーンのような問題だと、Alloy付属の標準ビジュアライザーの表示はあまり役に立ちません。ビジュアラザーの表示がそのまま使える例題は何かな？ と考えて、グラフの検索問題ならハマるだろうと。

ループ辺（同じ頂点に戻る辺）を許さない無向グラフのなかで、すべての頂点の次数（その頂点と接続している辺の数）が同じようなグラフを探すことにします。グラフの定義はAlloyと相性が良いので簡単に書けます。

-- 次数が一定のグラフ
module uniform_graph

-- グラフ（空グラフを除く）
some sig Graph {
 -- お隣さん（adjacent nodes）の集合
 adj: set Graph
} 

-- お隣さんの制約
fact {
 {
   -- 自分自身はお隣さんじゃない
   no (adj & iden)
  
   -- お隣さんは対称的な関係
   adj = ~adj
 }
}

-- 次数が一定
pred degree[n: Int] {
 all x: Graph |
   #(x.adj) = n
}  


/* コマンド */
run d2 {degree[2]} for 5
run d3 {degree[3]} for 6
run d4 {degree[4]} for 7

6頂点までのグラフで、次数が3のものを探すと、3つのグラフがみつかりました。そのうちの1つが次です。

小さい有限基数の台集合（underlying set）上の構造を列挙するときはAlloyが使えます。特に、ビジュアラザーの表示がそのまま意味を持つときは目視確認ができるので気分がいいですね。ビジュアラザー見てもナンダカわかんないときは気分悪いですが。