星11個の数独の問題をAlloyで

gistfile1.md

#星11個の数独の問題をAlloyで

解いたら3秒かかりませんでした．きっかけは 世界一難しい数独、Alloyで解いてみたよ(RocketNews24から) - dec9ue's diary の記事．処理に82秒かかったとあり「それって超難問では？」と思ったので，自分も動かしてみて，その結果を以下につらつらと．ちなみに下記AlloyのコードはAlloyのサンプルでそこら辺に転がっているのを移してきただけで，私のオリジナルではない．

abstract sig Number { data: Number -> Number }
abstract sig Region1, Region2, Region3 extends Number {}

one sig N1, N2, N3 extends Region1 {} 
one sig N4, N5, N6 extends Region2 {} 
one sig N7, N8, N9 extends Region3 {}

pred complete(rows: set Number,  cols: set Number) {
	Number in cols.(rows.data) 
}

pred rules() { 
	all x, y: Number { lone y.(x.data) }

	all row: Number { complete[row  , Number]  }
	all col: Number { complete[Number, col] }

	complete[Region1, Region1]
	complete[Region1, Region2]
	complete[Region1, Region3]
	complete[Region2, Region1]
	complete[Region2, Region2]
	complete[Region2, Region3]
	complete[Region3, Region1]
	complete[Region3, Region2]
	complete[Region3, Region3]
}

pred puzzle() { 
N1->N1->N8 + N2->N3->N3 + N2->N4->N6 +
N3->N2->N7 + N3->N5->N9 + N3->N7->N2 +
N4->N2->N5 + N4->N6->N7 + N5->N5->N4 +
N5->N6->N5 + N5->N7->N7 + N6->N4->N1 +
N6->N8->N3 + N7->N3->N1 + N7->N8->N6 +
N7->N9->N8 + N8->N3->N8 + N8->N4->N5 +
N8->N8->N1 + N9->N2->N9 + N9->N7->N4 in data
}
pred game() { rules[] && puzzle[] }
run game

初期条件pred_puzzle()の中身が問題を集合で表現している部分．「N1->N1->N8」なら座標(1, 1)には数字の8が入ります，という意味．処理時間は以下．

Executing "Run game"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   2725 vars. 729 primary vars. 3303 clauses. 508ms.
   . found. Predicate is consistent. 2681ms.

2.6秒でした．引用記事のコードと何が違うのかというと，エレメントNnを座標であると同時に中の数字としても扱っており，条件(ルール)の記述をシンプルに書いているせいかと．つまり条件complete()をうまく使っているのがカギ．こちらの方が分かりにくいね．ちなみに結果は以下．

...
this/Number<:data={N1$0->N1$0->N8$0, N1$0->N2$0->N1$0, N1$0->N3$0->N2$0, N1$0->N4$0->N7$0, N1$0->N5$0->N5$0, N1$0->N6$0->N3$0, N1$0->N7$0->N6$0, N1$0->N8$0->N4$0, N1$0->N9$0->N9$0, N2$0->N1$0->N9$0, N2$0->N2$0->N4$0, N2$0->N3$0->N3$0, N2$0->N4$0->N6$0, N2$0->N5$0->N8$0, N2$0->N6$0->N2$0, N2$0->N7$0->N1$0, N2$0->N8$0->N7$0, N2$0->N9$0->N5$0, N3$0->N1$0->N6$0, N3$0->N2$0->N7$0, N3$0->N3$0->N5$0, N3$0->N4$0->N4$0, N3$0->N5$0->N9$0, N3$0->N6$0->N1$0, N3$0->N7$0->N2$0, N3$0->N8$0->N8$0, N3$0->N9$0->N3$0, N4$0->N1$0->N1$0, N4$0->N2$0->N5$0, N4$0->N3$0->N4$0, N4$0->N4$0->N2$0, N4$0->N5$0->N3$0, N4$0->N6$0->N7$0, N4$0->N7$0->N8$0, N4$0->N8$0->N9$0, N4$0->N9$0->N6$0, N5$0->N1$0->N3$0, N5$0->N2$0->N6$0, N5$0->N3$0->N9$0, N5$0->N4$0->N8$0, N5$0->N5$0->N4$0, N5$0->N6$0->N5$0, N5$0->N7$0->N7$0, N5$0->N8$0->N2$0, N5$0->N9$0->N1$0, N6$0->N1$0->N2$0, N6$0->N2$0->N8$0, N6$0->N3$0->N7$0, N6$0->N4$0->N1$0, N6$0->N5$0->N6$0, N6$0->N6$0->N9$0, N6$0->N7$0->N5$0, N6$0->N8$0->N3$0, N6$0->N9$0->N4$0, N7$0->N1$0->N5$0, N7$0->N2$0->N2$0, N7$0->N3$0->N1$0, N7$0->N4$0->N9$0, N7$0->N5$0->N7$0, N7$0->N6$0->N4$0, N7$0->N7$0->N3$0, N7$0->N8$0->N6$0, N7$0->N9$0->N8$0, N8$0->N1$0->N4$0, N8$0->N2$0->N3$0, N8$0->N3$0->N8$0, N8$0->N4$0->N5$0, N8$0->N5$0->N2$0, N8$0->N6$0->N6$0, N8$0->N7$0->N9$0, N8$0->N8$0->N1$0, N8$0->N9$0->N7$0, N9$0->N1$0->N7$0, N9$0->N2$0->N9$0, N9$0->N3$0->N6$0, N9$0->N4$0->N3$0, N9$0->N5$0->N1$0, N9$0->N6$0->N8$0, N9$0->N7$0->N4$0, N9$0->N8$0->N5$0, N9$0->N9$0->N2$0}
...

見方は，たとえば「N1$0->N2$0->N1$0」なら，座標(1, 2)には数字の1が入ります，という意味．$0は無視してOK．これだと見にくいので，加工用のPythonをサクッと．なんか変だけど動けば良いというノリで．

#! /usr/bin/python
import sys

f = open('result.txt', 'r')

cells = []

for line in f:
	cells.append(line.split(','))
f.close()

cells_ = cells[0]

for i in range(len(cells_)):
	print ' ' + str(cells_[i][int(cells_[i].rfind('->')) + 3]) + ' ',
	if i % 3 == 2 and i % 9 != 8:
		print '|',
	if i % 9 == 8:
		print ''
	if i % 27 == 26 and i != 80:
		print '------------+-------------+------------'

ついでに，数独の問題をAlloyのコードに加工するPythonのコードは以下．起動すると一行ずつ入力を求められるので，9桁の数字(空白は半角スペース)を打ち込む，という仕様．

#!/usr/bin/ python
import sys

def input_rows(i):
	row_string = raw_input(str(i + 1) + ' row: ')
	if (len(row_string) != 9):
		row_string = input_rows(i)
	return row_string

row = []
for i in range(9):
	row_string = input_rows(i)
	row.append(row_string)

code_to_alloy = []
def convert_and_confirm(rows):
	for j in range(len(rows)):
		for k in range(len(rows[j])):
			print ' ' + str(rows[j][k]) + ' ',
			if k % 3 == 2 and k != 8:
				print '|',
			if k % 9 == 8:
				print ''
			code = ''
			if rows[j][k] != ' ':
				code = 'N' + str(j + 1) + '->N' + str(k + 1) + '->N' + str(rows[j][k])
				code_to_alloy.append(code)
		if j % 3 == 2 and j != 8:
			print '------------+-------------+------------'

def display_to_alloy(codes):
	for l in range(len(codes)):
		print codes[l],
		if l != len(codes) - 1:
			if l % 3 != 2:
				print '+',
			else:
				print '+'
		else:
			print 'in data'

print convert_and_confirm(row)
print display_to_alloy(code_to_alloy)

Noneとかまで出力されるけど気にしない気にしない．