Alloyで数独

sudoku.als

enum CellPositionNum { CP1, CP2, CP3 }

enum CellValue { CV1, CV2, CV3, CV4, CV5, CV6, CV7, CV8, CV9 }

one sig Board {
	board : CellPositionNum -> CellPositionNum -> CellPositionNum -> CellPositionNum -> CellValue
} {
	all a,b,c,d:CellPositionNum | one board[a,b,c,d]
	all a,b:CellPositionNum, v:CellValue | one c,d:CellPositionNum | board[a,b,c,d] = v
	all c,d:CellPositionNum, v:CellValue | one a,b:CellPositionNum | board[a,b,c,d] = v
	all a,c:CellPositionNum, v:CellValue | one b,d:CellPositionNum | board[a,b,c,d] = v
}

run {
	(CP1->CP1->CP1->CP3->CV5) in Board.board
	(CP1->CP1->CP2->CP1->CV3) in Board.board
	(CP1->CP2->CP1->CP1->CV8) in Board.board
	(CP1->CP2->CP3->CP2->CV2) in Board.board
	(CP1->CP3->CP1->CP2->CV7) in Board.board
	(CP1->CP3->CP2->CP2->CV1) in Board.board
	(CP1->CP3->CP3->CP1->CV5) in Board.board
	(CP2->CP1->CP1->CP1->CV4) in Board.board
	(CP2->CP1->CP2->CP3->CV5) in Board.board
	(CP2->CP1->CP3->CP1->CV3) in Board.board
	(CP2->CP2->CP1->CP2->CV1) in Board.board
	(CP2->CP2->CP2->CP2->CV7) in Board.board
	(CP2->CP2->CP3->CP3->CV6) in Board.board
	(CP2->CP3->CP1->CP3->CV3) in Board.board
	(CP2->CP3->CP2->CP1->CV2) in Board.board
	(CP2->CP3->CP3->CP2->CV8) in Board.board
	(CP3->CP1->CP1->CP2->CV6) in Board.board
	(CP3->CP1->CP2->CP1->CV5) in Board.board
	(CP3->CP1->CP3->CP3->CV9) in Board.board
	(CP3->CP2->CP1->CP3->CV4) in Board.board
	(CP3->CP2->CP3->CP2->CV3) in Board.board
	(CP3->CP3->CP2->CP3->CV9) in Board.board
	(CP3->CP3->CP3->CP1->CV7) in Board.board
} for 10