Alloy Analyzer について軽く文法を調べれたので，試しに動かしてみました．

サンプル

問題

A, B, C, D の 4 人は，総務，外務，財務，防衛の 4 つの大臣に重複なく割り振られる．割り振りに関して，以下の情報が得られた：

1. B の担当は外務大臣でも財務大臣でもない;
2. 総務大臣の担当は A か D;
3. D の担当は財務大臣か防衛大臣．

さて，割り振りはどうなっていたか？

解答

まずは，普通に解いていきます．

3 から，D は総務大臣ではないので，2 より A が総務大臣となります．

あとは外務，財務，防衛の 3 個の候補が残っていますが，1 より B は外務でも財務でもないので，B は防衛と定まります．

再び 3 より，D の候補は財務に絞られるので，D が財務大臣となり，C は残った外務大臣となります．

Alloy で解いてみた

まずは，ホニャララ大臣を定義します：

// 大臣
abstract sig Minister {}
one sig Soumu extends Minister {}
one sig Gaimu extends Minister {}
one sig Zaimu extends Minister {}
one sig Bouei extends Minister {}

次に，人を定義します：

// 人
abstract sig Person {
    tantou:  one Minister
}
one sig A extends Person {}
one sig B extends Person {}
one sig C extends Person {}
one sig D extends Person {}

条件についてですが，問題文の 3 個の他に，それぞれ異なる大臣になる，という条件もあるので，合わせて記述します．これらは確定事項なので，fact として記述します：

// ファクト
fact fact1 {
    B.tantou != Gaimu && B.tantou != Zaimu
}

fact fact2 {
    A.tantou = Soumu || D.tantou = Soumu
}

fact fact3 {
    D.tantou = Zaimu || D.tantou = Bouei
}

fact distinctTantou {
    A.tantou != B.tantou &&
    A.tantou != C.tantou &&
    A.tantou != D.tantou &&
    B.tantou != C.tantou &&
    B.tantou != D.tantou &&
    C.tantou != D.tantou
}

って，distinctTantou の書き方がダサすぎる（名前もダサいのは置いといて！！！）．
以下のように pred を使って書き直します：

fact distinctTantou {
    /*
    A.tantou != B.tantou &&
    A.tantou != C.tantou &&
    A.tantou != D.tantou &&
    B.tantou != C.tantou &&
    B.tantou != D.tantou &&
    C.tantou != D.tantou
    */
    all a, b: one Person | neq[a, b]
}

pred neq [a, b: one Person] {
    a != b implies a.tantou != b.tantou
}

最後に，表示用の pred を記述して run すれば OK.

全体像は以下の通り：

// 大臣
abstract sig Minister {}
one sig Soumu extends Minister {}
one sig Gaimu extends Minister {}
one sig Zaimu extends Minister {}
one sig Bouei extends Minister {}

// 人
abstract sig Person {
    tantou:  one Minister
}
one sig A extends Person {}
one sig B extends Person {}
one sig C extends Person {}
one sig D extends Person {}

// ファクト
fact fact1 {
    B.tantou != Gaimu && B.tantou != Zaimu
}

fact fact2 {
    A.tantou = Soumu || D.tantou = Soumu
}

fact fact3 {
    D.tantou = Zaimu || D.tantou = Bouei
}

// だっさ！！！！！
fact distinctTantou {
    /*
    A.tantou != B.tantou &&
    A.tantou != C.tantou &&
    A.tantou != D.tantou &&
    B.tantou != C.tantou &&
    B.tantou != D.tantou &&
    C.tantou != D.tantou
    */
    all a, b: one Person | neq[a, b]
}

pred neq [a, b: one Person] {
    a != b implies a.tantou != b.tantou
}

pred show {}

run show

そんで，出てきたのが以下の図：

正しく表示されてるし，Next を押しても他の例が表示されない！やったね！