Alloyで論理パズルを生成

Alloyで論理パズルを解くのではなく、Alloyに論理パズルを作らせたい。

ここしばらく考えていたのだけども、なかなか行きの電車で座れなかったので(ぇ)解けなかったのだが、今日は妙に電車が空いていたので座ってゆっくり考えることができた。

「解が一意になるような制約を探す」ってのは「制約を満たすような実例を探す」という普通のAlloyの使い方と比較してみるとAlloyの出す実例とは今回の場合『制約』だということがわかる。そこまではよかったのだけどその先がしばらくわからなかった。

enum Person {X, Y, Z}

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

それはこのAlloyのプログラムに入れるべき制約、つまり『解が一意になる』の表現方法だ。普通に書くとAlloyは「解がない」と答えるか「解がある、たとえばこれ」と1個出してくるかしかしない。全部の可能な解をリストアップして、その個数が1個であることを宣言するにはどうすればいいか？

肝はAlloyの中で暗黙に行われている列挙を明示的にコードで書くこと。肝に気付いてしまえば実装は意外と簡単だ。「パラメータのすべての可能な組み合わせのうち、制約を満たすものがanswersである。「let answers = {x, y, z: Bool | satisfy[constrains, x, y, z]}」というだけのこと。引数に制約自体を渡しているのは将来的に「解を一意にする最小の制約である」って制約を付けたいから。パズルに必要ないヒントがあるのはダサいからね。

というわけでコードはたった33行。1週間近く悩んでたとは思えない。

enum Person {X, Y, Z}
enum Bool {T, F}

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

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

run {
	let answers = {
		x, y, z: Bool | 
		satisfy[Constrain, x, y, z]}{

		one answers
	}
}

これを実行すると、「XはXを嘘つきだといった」(Xが正直だとすると矛盾するのでXが嘘つき)とか「XはYとZが嘘つきだといった」(嘘つきは1人というルールなのでXが嘘つき)とかが出力される。確かに。もっと複雑なパズルがいいので「自分を嘘つきだとは言わない」「嘘つきだと指摘するのは一度に1人」って制約を入れてみよう。

fact {
	all c: Constrain {
		c.by not in c.who
		one c.who
	}
}

これで「XがYを嘘つきだといい、YがZを嘘つきだといった」ってパズルが出力される。

もっと人数を増やしてパズルの難易度を上げてみたいけど現状の実装だと人数を増やすのが面倒だな。それをどうすればいいかは今後考える。