Alloyでそれなりの難易度の論理パズルを生成 - 西尾泰和のはてなダイアリー

Alloyを使って生成したパズル

Q1

E: AとBは嘘つきだよ
B: え、Aは嘘つきだけど僕は違うよ
A: 私だって嘘つきではないわ
D: Aは嘘つきだよね。あとEも嘘つき。
C: 僕は嘘つきではないよ！！

この中に嘘つきが2人います。嘘つきは嘘をついたり本当のことを言ったりします。嘘つきでない人は嘘をつきません。

正解はコードの後。

コード

enum Person {A, B, C, D, E}
enum Bool {T, F}

// 制約
abstract sig Constrain{}
// 「Xが『Yは嘘つきだ』と言った」という制約
sig is_liar extends Constrain {
	by: one Person,
	who: one Person
}{
	by not in who
}


// 与えられたx, y, zの真偽値の対が制約を満たすかどうか返す
// 引数を変えて試すため、述語にくくり出されている必要がある
pred satisfy(cs: Constrain, a, b, c, d, e: Bool){
	let p2b = (A -> a) + (B -> b) + (C -> c) +
		(D -> d) + (E -> e)
		{
		// 嘘つきの人数を指定
		#{p2b.F} = 3
		// すべての制約について、発言者が正直なら充足される
		// 今は「whoは嘘つき」しかない
		all c: cs{
			(c.by.p2b = T) => (c.who.p2b = F)
		}
	}
}



run {
	let answers = {
		a, b, c, d, e: Bool | 
		satisfy[Constrain, a, b, c, d, e]}
		{

		// 解は一つ
		one answers

		// どの制約を取り除いても解は一つではなくなる
		all x: Constrain {
			not one {
				a, b, c, d, e: Bool | 
				satisfy[Constrain - x, a, b, c, d, e]
			}
		}
	}
} for 10

Q1解答編

AとEが嘘つきですね。問題をもう一度見てみましょう。

Aが正直だとするとAを嘘つきだといっているE, B, Dの3人が嘘つきだということになって「嘘つきは2人」という条件と矛盾する。Eが正直だとすると、AとBが嘘つきなのだが、DはEを嘘つきと呼んでいるのでDも嘘つきになる。やはり「嘘つきは2人」という条件と矛盾する。AとEが嘘つきという条件では矛盾が起きない。

Q2

C: Aは嘘つきだ
A: 違うよ、Dだよ
D: Cはとりあえず嘘つきだよね。あとBとEも。
B: え、嘘つきなのはAとCだよ。
E: うん、同意。嘘つきなのはAとCだよね。

嘘つきが3人います。

Q3

Q2ではBとEが同じ事を言ってたので、それは禁止してみた。あと一人の人が三人以上を嘘つき呼ばわりすると「たぶんこいつは嘘つきだろうな」とかguessされちゃうので禁止してみた。逆に三人を嘘つきだと言っている人が正直である例を探させることもできたけど、先にコードを出すと答えがバレるし。

fact {
	// 違う人は違うことを言う
	all disj p1, p2: Person {
		by.p1 != by.p2
	}
	// 一人の人は3人以上を嘘つき呼ばわりしない
	all p: Person {
		#{by.p} < 3
	}
}

B: Aが嘘つきだ。
A: いや、私は違う。Dが嘘つきだよ。
D: Bがそもそも嘘つきだよ。あとCも。
C: いやいや、AとBが両方嘘つきなんだよ
A: ちなみにEも嘘つきだ。
E: ええー、違うよ。CとDが嘘つきなんだよ。

嘘つきは3人います。

まとめ

Alloyで61行くらい記述して0.6秒くらい実行すると、これくらいの難易度のパズルを生成することができる。

Generating the solution...
   3537 vars. 110 primary vars. 6552 clauses. 343ms.
   ... is consistent. 353ms.

エレガントな解答

xが正直である場合、xが嘘つきだといった人もxを嘘つきだといった人も嘘つきに確定するので、実は無向グラフとしてみた場合に位数が4以上の頂点は正直者たりえない。Q3のグラフを書けばA, C, Dの位数が4、B, Eの位数が3なのでA, C, Dが嘘つきと決まる。