A Sudoku Solver in Alloy

A couple of days ago I got stuck doing the sudoku in the Evening Standard.  Normally I just work my way through these puzzles by lightly pencilling in all the possible numbers and then systematically eliminating and erasing possibilities until only one remains for each square.  However, this time, I reached a point from which I just could not see any way to progress.  I would normally have taken this as a sign that I had made a mistake, and erased everything and started again.  But, instead I decided to write an Alloy model to solve sudoku once and for all.  In that way I hoped to cure myself of wasting time on these pointless little puzzles.

/* Sudoku.als - A Sudoku Solver on Alloy */


abstract sig Cols {}
one sig c1, c2, c3, c4, c5, c6, c7, c8, c9 extends Cols {}


abstract sig Rows {}
one sig r1, r2, r3, r4, r5, r6, r7, r8, r9 extends Rows {}


abstract sig Boxes {}
one sig b11, b12, b13, b21, b22, b23, b31, b32, b33 extends Boxes {}


abstract sig Nums {}
one sig n1, n2, n3, n4, n5, n6, n7, n8, n9 extends Nums {}


abstract sig Cells {
	col : Cols,
	row : Rows,
	box : Boxes,
	num : Nums
}

one sig c11, c12, c13, c14, c15, c16, c17, c18, c19 extends Cells {}
one sig c21, c22, c23, c24, c25, c26, c27, c28, c29 extends Cells {}
one sig c31, c32, c33, c34, c35, c36, c37, c38, c39 extends Cells {}
one sig c41, c42, c43, c44, c45, c46, c47, c48, c49 extends Cells {}
one sig c51, c52, c53, c54, c55, c56, c57, c58, c59 extends Cells {}
one sig c61, c62, c63, c64, c65, c66, c67, c68, c69 extends Cells {}
one sig c71, c72, c73, c74, c75, c76, c77, c78, c79 extends Cells {}
one sig c81, c82, c83, c84, c85, c86, c87, c88, c89 extends Cells {}
one sig c91, c92, c93, c94, c95, c96, c97, c98, c99 extends Cells {}

fact Col_structure {
	(c11+c21+c31+c41+c51+c61+c71+c81+c91).col in c1 and
	(c12+c22+c32+c42+c52+c62+c72+c82+c92).col in c2 and
	(c13+c23+c33+c43+c53+c63+c73+c83+c93).col in c3 and
	(c14+c24+c34+c44+c54+c64+c74+c84+c94).col in c4 and
	(c15+c25+c35+c45+c55+c65+c75+c85+c95).col in c5 and
	(c16+c26+c36+c46+c56+c66+c76+c86+c96).col in c6 and
	(c17+c27+c37+c47+c57+c67+c77+c87+c97).col in c7 and
	(c18+c28+c38+c48+c58+c68+c78+c88+c98).col in c8 and
	(c19+c29+c39+c49+c59+c69+c79+c89+c99).col in c9
}

fact Row_structure {
	(c11+c12+c13+c14+c15+c16+c17+c18+c19).row in r1 and
	(c21+c22+c23+c24+c25+c26+c27+c28+c29).row in r2 and
	(c31+c32+c33+c34+c35+c36+c37+c38+c39).row in r3 and
	(c41+c42+c43+c44+c45+c46+c47+c48+c49).row in r4 and
	(c51+c52+c53+c54+c55+c56+c57+c58+c59).row in r5 and
	(c61+c62+c63+c64+c65+c66+c67+c68+c69).row in r6 and
	(c71+c72+c73+c74+c75+c76+c77+c78+c79).row in r7 and
	(c81+c82+c83+c84+c85+c86+c87+c88+c89).row in r8 and
	(c91+c92+c93+c94+c95+c96+c97+c98+c99).row in r9
}

fact Box_structure {
	(c11+c12+c13+c21+c22+c23+c31+c32+c33).box in b11 and
	(c14+c15+c16+c24+c25+c26+c34+c35+c36).box in b12 and
	(c17+c18+c19+c27+c28+c29+c37+c38+c39).box in b13 and
	(c41+c42+c43+c51+c52+c53+c61+c62+c63).box in b21 and
	(c44+c45+c46+c54+c55+c56+c64+c65+c66).box in b22 and
	(c47+c48+c49+c57+c58+c59+c67+c68+c69).box in b23 and
	(c71+c72+c73+c81+c82+c83+c91+c92+c93).box in b31 and
	(c74+c75+c76+c84+c85+c86+c94+c95+c96).box in b32 and
	(c77+c78+c79+c87+c88+c89+c97+c98+c99).box in b33
}


fact Rules_of_the_game {
	no disj c1, c2 : Cells |
		c1.num = c2.num and
		(c1.col = c2.col or c1.row = c2.row or c1.box = c2.box)
}


pred EveningStandard20120404 {
	/*
	+-------+-------+-------+
	| _ 7 _ | 5 _ 8 | _ _ _ |
	| _ 9 _ | _ _ _ | _ _ _ |
	| 3 _ 2 | 1 _ _ | _ 9 _ |
	+-------+-------+-------+
	| 7 _ 6 | _ _ _ | _ _ 8 |
	| _ _ _ | 4 _ 5 | _ _ _ |
	| 5 _ _ | _ _ _ | 9 _ 4 |
	+-------+-------+-------+
	| _ 3 _ | _ _ 2 | 5 _ 7 |
	| _ _ _ | _ _ _ | _ 2 _ |
	| _ _ _ | 6 _ 4 | _ 3 _ |
	+-------+-------+-------+
	*/
	c12.num in n7 and c14.num in n5 and c16.num in n8 and
	c22.num in n9 and
	c31.num in n3 and c33.num in n2 and c34.num in n1 and c38.num in n9 and
	c41.num in n7 and c43.num in n6 and c49.num in n8 and
	c54.num in n4 and c56.num in n5 and
	c61.num in n5 and c67.num in n9 and c69.num in n4 and
	c72.num in n3 and c76.num in n2 and c77.num in n5 and c79.num in n7 and
	c88.num in n2 and
	c94.num in n6 and c96.num in n4 and c98.num in n3
}


run {EveningStandard20120404} for 9 Cols, 9 Rows, 9 Boxes, 9 Nums, 81 Cells

	/*
	This gives the following solution, expressed as a predicate (see the Txt display):

	this/Cells<:num={
		c11$0->n6$0, c12$0->n7$0, c13$0->n1$0, c14$0->n5$0, c15$0->n9$0, c16$0->n8$0, c17$0->n2$0, c18$0->n4$0, c19$0->n3$0,
		c21$0->n4$0, c22$0->n9$0, c23$0->n5$0, c24$0->n7$0, c25$0->n2$0, c26$0->n3$0, c27$0->n1$0, c28$0->n8$0, c29$0->n6$0,
		c31$0->n3$0, c32$0->n8$0, c33$0->n2$0, c34$0->n1$0, c35$0->n4$0, c36$0->n6$0, c37$0->n7$0, c38$0->n9$0, c39$0->n5$0,
		c41$0->n7$0, c42$0->n4$0, c43$0->n6$0, c44$0->n2$0, c45$0->n1$0, c46$0->n9$0, c47$0->n3$0, c48$0->n5$0, c49$0->n8$0,
		c51$0->n9$0, c52$0->n1$0, c53$0->n8$0, c54$0->n4$0, c55$0->n3$0, c56$0->n5$0, c57$0->n6$0, c58$0->n7$0, c59$0->n2$0,
		c61$0->n5$0, c62$0->n2$0, c63$0->n3$0, c64$0->n8$0, c65$0->n6$0, c66$0->n7$0, c67$0->n9$0, c68$0->n1$0, c69$0->n4$0,
		c71$0->n1$0, c72$0->n3$0, c73$0->n4$0, c74$0->n9$0, c75$0->n8$0, c76$0->n2$0, c77$0->n5$0, c78$0->n6$0, c79$0->n7$0,
		c81$0->n8$0, c82$0->n6$0, c83$0->n7$0, c84$0->n3$0, c85$0->n5$0, c86$0->n1$0, c87$0->n4$0, c88$0->n2$0, c89$0->n9$0,
		c91$0->n2$0, c92$0->n5$0, c93$0->n9$0, c94$0->n6$0, c95$0->n7$0, c96$0->n4$0, c97$0->n8$0, c98$0->n3$0, c99$0->n1$0
	}
	Expressed as a diagram the solution is:
	+-------+-------+-------+
	| 6 7 1 | 5 9 8 | 2 4 3 |
	| 4 9 5 | 7 2 3 | 1 8 6 |
	| 3 8 2 | 1 4 6 | 7 9 5 |
	+-------+-------+-------+
	| 7 4 6 | 2 1 9 | 3 5 8 |
	| 9 1 8 | 4 3 5 | 6 7 2 |
	| 5 2 3 | 8 6 7 | 9 1 4 |
	+-------+-------+-------+
	| 1 3 4 | 9 8 2 | 5 6 7 |
	| 8 6 7 | 3 5 1 | 4 2 9 |
	| 2 5 9 | 6 7 4 | 8 3 1 |
	+-------+-------+-------+
	Finding this solution took 12s on a laptop with a 1.4GHz processor.
	No further solutions were found.
	*/

The definition of this/Cells in the last comment overflows the right margin, so I have also included a full copy of the source file here.

I used named atoms to represent not only the cells, rows, columns and boxes, but also the numbers that go in the cells.  It might seem more obvious to use integers  to represent the numbers but we do not need the full properties of integers (or of natural numbers).  All we need is to be able to test whether or not two numbers are the same, and for this named atoms are adequate.  Sudoku would still work if you had to fill the cells with letters, or even colours.

If I was writing a sudoku solver in a proper programming language I would certainly use integers instead of named atoms.  This would enable me to calculate the row, column and box structures, instead of manually enumerating them, which would make things less error-prone.

One thing that surprised me was the shortness of the Rules_of_the_game definition: just three lines.  Alloy is good at capturing the essence of a system in a very succinct expression.

 As you can see, I ran the model on the Evening Standard puzzle and it produced a solution.  I checked the solution manually and it was correct.  I got Alloy to look for further solutions and it couldn't find any, so the solution was unique.  I compared the solution with my attempt and I had not made any mistakes, but the solution gave no hint on how I could make progress from the position I had got to.  The model gave a solution but gave no insight as to how to get to that solution.  So the model didn't really solve my problem, which was that of finding the next move in a given position.  But I will leave that problem to the reader.  I might get round to looking at it some day.