Instantly share code, notes, and snippets.

Embed
What would you like to do?
Solving sudoku in alloy
enum V {v1, v2, v3, v4, v5, v6, v7, v8, v9}
sig Cell {
val: V,
row: V,
col: V
}
pred disjointSubgrid[rows: set V, cols: set V]{
no disj c1, c2: Cell {
c1.row in rows
c2.row in rows
c1.col in cols
c2.col in cols
c1.val = c2.val
}
}
fact sudoku {
#Cell = 81
//One cell per grid location
no disj x, y: Cell | x.col = y.col and x.row = y.row
//distinct values per column and row
no disj x, y: Cell | x.val = y.val and (x.col = y.col or x.row = y.row)
//distinct values per subgrid
let s1 = (v1 + v2 + v3) | let s2 = (v4 + v5 + v6) | let s3 = (v7 + v8 + v9) {
disjointSubgrid[s1, s1]
disjointSubgrid[s1, s2]
disjointSubgrid[s1, s3]
disjointSubgrid[s2, s1]
disjointSubgrid[s2, s2]
disjointSubgrid[s2, s3]
disjointSubgrid[s3, s1]
disjointSubgrid[s3, s2]
disjointSubgrid[s3, s3]
}
}
// * 2 3 * * 8 * 5 *
// * 8 * 9 * * 4 7 *
// * * * 5 * * * * *
// * 9 1 * 3 * * * *
// * * * 8 * * 5 * 6
// * * * * * 4 * * *
// * * * * 6 * * * *
// 7 * 9 * 8 * * * 5
// 6 * * * * 2 3 * 8
fact puzzle {
one c: Cell | c.row = v1 and c.col = v2 and c.val = v2
one c: Cell | c.row = v1 and c.col = v3 and c.val = v3
one c: Cell | c.row = v1 and c.col = v6 and c.val = v8
one c: Cell | c.row = v1 and c.col = v8 and c.val = v5
one c: Cell | c.row = v2 and c.col = v2 and c.val = v8
one c: Cell | c.row = v2 and c.col = v4 and c.val = v9
one c: Cell | c.row = v2 and c.col = v7 and c.val = v4
one c: Cell | c.row = v2 and c.col = v8 and c.val = v7
one c: Cell | c.row = v3 and c.col = v4 and c.val = v5
one c: Cell | c.row = v4 and c.col = v2 and c.val = v9
one c: Cell | c.row = v4 and c.col = v3 and c.val = v1
one c: Cell | c.row = v4 and c.col = v5 and c.val = v3
one c: Cell | c.row = v5 and c.col = v4 and c.val = v8
one c: Cell | c.row = v5 and c.col = v7 and c.val = v5
one c: Cell | c.row = v5 and c.col = v9 and c.val = v6
one c: Cell | c.row = v6 and c.col = v6 and c.val = v4
one c: Cell | c.row = v7 and c.col = v5 and c.val = v6
one c: Cell | c.row = v8 and c.col = v1 and c.val = v7
one c: Cell | c.row = v8 and c.col = v3 and c.val = v9
one c: Cell | c.row = v8 and c.col = v5 and c.val = v8
one c: Cell | c.row = v8 and c.col = v9 and c.val = v5
one c: Cell | c.row = v9 and c.col = v1 and c.val = v6
one c: Cell | c.row = v9 and c.col = v6 and c.val = v2
one c: Cell | c.row = v9 and c.col = v7 and c.val = v3
one c: Cell | c.row = v9 and c.col = v9 and c.val = v8
}
pred show {}
run show for 81 but 8 Int
//Takes 26 seconds with cells constrained to 81 (but only works when "prevent overflow" is turned off, or when Int is set to bitwidth 8 or above)
//takes 50 seconds without cells constrained to 81 (but works regardless of "prevent overflow")
// (->> (str/split "* 2 3 * * 8 * 5 *
// * 8 * 9 * * 4 7 *
// * * * 5 * * * * *
// * 9 1 * 3 * * * *
// * * * 8 * * 5 * 6
// * * * * * 4 * * *
// * * * * 6 * * * *
// 7 * 9 * 8 * * * 5
// 6 * * * * 2 3 * 8" #"\n")
// (map-indexed (fn [row s]
// (->> (str/split s #"\s")
// (map-indexed (fn [col v]
// {:row row :col col :val v})))))
// flatten
// (filter #(not= "*" (:val %)))
// (mapv (fn [{:keys [row col val]}]
// (printf "one c: Cell | c.row = v%d and c.col = v%d and c.val = v%s\n" (inc row) (inc col) val))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment