Sudoku solving in Alloy

sudoku.als

sig Number {} 
sig Group {contains: disj set Number} {
	#contains = 3
}

one sig Board {
	assign: Number -> Number -> one Number
} {
	all n, x: Number | one assign.n & x -> Number
	all n, y: Number | one assign.n & Number -> y
	all n: Number, gx,gy: Group | one assign.n & gx.contains -> gy.contains
}


pred example {
	-- https://www.researchgate.net/figure/Example-smallest-sudoku-asymmetrical-n-17_fig3_259604903
	some disj g1,g2,g3: Group {
		some disj n1,n2,n3,n4,n5,n6,n7,n8,n9: Number {
			g1.contains = n1+n2+n3
			g2.contains = n4+n5+n6
			g3.contains = n7+n8+n9
			let clues = n1->(n2->n6 + n5->n2 + n9->n7) +
				n2->(n4->n5 + n8->n3) +
				n4->(n4->n1 + n6->n3) +
				n5->(n2->n2 + n3->n7 + n7->n4) +
				n6->n4->n8 +
				n7->(n5->n6 + n7->n2) +
				n8->(n1->n3 + n6->n7) +
				n9->n1->n1 |
					clues in Board.assign
		}
	}
}

run {example} for exactly 9 Number, exactly 3 Group