Skip to content

Instantly share code, notes, and snippets.

@lynaghk lynaghk/sudoku.als
Created Jul 18, 2018

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
You can’t perform that action at this time.