even/odd killer sudoku
https://www.youtube.com/post/UgzibAW-6ZvjcvdLLk94AaABCQ
diff --git a/sentient/package.json b/sentient/package.json
new file mode 100644
index 0000000..d076275
--- /dev/null
+++ b/sentient/package.json
@@ -0,0 +1,9 @@
+{
+ "name": "sentient",
+ "version": "1.0.0",
+ "main": "index.js",
+ "license": "MIT",
+ "devDependencies": {
+ "sentient-lang": "^0.0.0-beta.1"
+ }
+}
diff --git a/sentient/sudoku.snt b/sentient/sudoku.snt
new file mode 100644
index 0000000..d2f9cac
--- /dev/null
+++ b/sentient/sudoku.snt
@@ -0,0 +1,59 @@
+array9<array9<int5>> X;
+
+X.each(function (row) {
+ row.each(function (cell) {
+ invariant cell.between?(1, 9);
+ });
+});
+
+function valid?(ary) {
+ invariant ary.uniq?;
+};
+
+boxes = [];
+[0, 3, 6].each(function^ (x) {
+ [0, 3, 6].each(function^ (y) {
+ boxes = boxes.push([
+ X[y ][x], X[y ][x+1], X[y ][x+2],
+ X[y+1][x], X[y+1][x+1], X[y+1][x+2],
+ X[y+2][x], X[y+2][x+1], X[y+2][x+2]
+ ]);
+ });
+});
+
+X.each(*valid?);
+X.transpose.each(*valid?);
+boxes.each(*valid?);
+
+# Now the extras...
+
+# evens
+invariant X[0][3] % 2 == 0;
+invariant X[0][7] % 2 == 0;
+invariant X[2][1] % 2 == 0;
+invariant X[2][5] % 2 == 0;
+invariant X[4][3] % 2 == 0;
+invariant X[4][7] % 2 == 0;
+invariant X[6][1] % 2 == 0;
+invariant X[6][5] % 2 == 0;
+invariant X[8][3] % 2 == 0;
+
+invariant X[1][2] % 2 == 1;
+invariant X[1][6] % 2 == 1;
+invariant X[3][0] % 2 == 1;
+invariant X[3][4] % 2 == 1;
+invariant X[3][8] % 2 == 1;
+invariant X[5][2] % 2 == 1;
+invariant X[5][6] % 2 == 1;
+invariant X[7][0] % 2 == 1;
+invariant X[7][4] % 2 == 1;
+
+invariant X[0][5] + X[1][4] + X[2][3] + X[3][2] + X[4][1] + X[5][0] == 45;
+invariant X[1][0] + X[2][1] + X[3][2] + X[4][3] + X[5][4] + X[6][5] + X[7][6] + X[8][7] == 56;
+invariant X[3][0] + X[4][1] + X[5][2] + X[6][3] + X[7][4] + X[8][5] == 18;
+invariant X[0][6] + X[1][7] + X[2][8] == 11;
+invariant X[0][3] + X[1][4] + X[2][5] + X[3][5] + X[4][7] + X[5][8] == 24;
+invariant X[2][8] + X[3][7] + X[4][6] + X[5][5] + X[6][4] + X[7][3] + X[8][2] == 25;
+invariant X[6][8] + X[7][7] + X[8][6] == 8;
+
+expose X;
diff --git a/sentient/yarn.lock b/sentient/yarn.lock
new file mode 100644
index 0000000..05bc07d
--- /dev/null
+++ b/sentient/yarn.lock
@@ -0,0 +1,27 @@
+# THIS IS AN AUTOGENERATED FILE. DO NOT EDIT THIS FILE DIRECTLY.
+# yarn lockfile v1
+
+
+colors@^1.1.2:
+ version "1.4.0"
+ resolved "https://registry.yarnpkg.com/colors/-/colors-1.4.0.tgz#c50491479d4c1bdaed2c9ced32cf7c7dc2360f78"
+ integrity sha512-a+UqTh4kgZg/SlGvfbzDHpgRu7AAQOmmqRHJnxhRZICKFUT91brVhNNt58CMWU9PsBbv3PDCZUHbVxuDiH2mtA==
+
+commander@^2.9.0:
+ version "2.20.3"
+ resolved "https://registry.yarnpkg.com/commander/-/commander-2.20.3.tgz#fd485e84c03eb4881c20722ba48035e8531aeb33"
+ integrity sha512-GpVkmM8vF2vQUkj2LvZmD35JxeJOLCwJ9cUkugyk2nuhbv3+mJvpLYYt+0+USMxE+oj+ey/lJEnhZw75x/OMcQ==
+
+sentient-lang@^0.0.0-beta.1:
+ version "0.0.0-beta.1"
+ resolved "https://registry.yarnpkg.com/sentient-lang/-/sentient-lang-0.0.0-beta.1.tgz#fc59d8a04dd3d162aa92ef380011d21bb96fa3fb"
+ integrity sha512-X905ZT860woccfhNFSm/m7EOqKF9LkSTnPzfck0ECN//bbZwIrTIVwh409ci+BMeJxpyHDuPv2spzkdwt+omng==
+ dependencies:
+ colors "^1.1.2"
+ commander "^2.9.0"
+ underscore "^1.8.3"
+
+underscore@^1.8.3:
+ version "1.10.2"
+ resolved "https://registry.yarnpkg.com/underscore/-/underscore-1.10.2.tgz#73d6aa3668f3188e4adb0f1943bd12cfd7efaaaf"
+ integrity sha512-N4P+Q/BuyuEKFJ43B9gYuOj4TQUHXX+j2FqguVOpjkssLUUrnJofCcBccJSCoeturDoZU6GorDTHSvUDlSQbTg==
diff --git a/z3/sudoku.py b/z3/sudoku.py
new file mode 100644
index 0000000..d37b147
--- /dev/null
+++ b/z3/sudoku.py
@@ -0,0 +1,85 @@
+from z3 import *
+
+# 9x9 matrix of integer variables
+X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
+ for i in range(9) ]
+
+# each cell contains a value in {1, ..., 9}
+cells_c = [ And(1 <= X[i][j], X[i][j] <= 9)
+ for i in range(9) for j in range(9) ]
+
+# each row contains a digit at most once
+rows_c = [ Distinct(X[i]) for i in range(9) ]
+
+# each column contains a digit at most once
+cols_c = [ Distinct([ X[i][j] for i in range(9) ])
+ for j in range(9) ]
+
+# each 3x3 square contains a digit at most once
+sq_c = [ Distinct([ X[3*i0 + i][3*j0 + j]
+ for i in range(3) for j in range(3) ])
+ for i0 in range(3) for j0 in range(3) ]
+
+sudoku_c = cells_c + rows_c + cols_c + sq_c
+
+# # sudoku instance, we use '0' for empty cells
+# instance = ((0,0,0,0,0,0,0,0,0),
+# (0,0,0,0,0,0,0,0,0),
+# (0,0,0,0,0,0,0,0,0),
+# (0,0,0,0,0,0,0,0,0),
+# (0,0,0,0,0,0,0,0,0),
+# (0,0,0,0,0,0,0,0,0),
+# (0,0,0,0,0,0,0,0,0),
+# (0,0,0,0,0,0,0,0,0),
+# (0,0,0,0,0,0,0,0,0))
+
+# instance_c = [ If(instance[i][j] == 0,
+# True,
+# X[i][j] == instance[i][j])
+# for i in range(9) for j in range(9) ]
+
+evens_c = [
+ X[0][3] % 2 == 0,
+ X[0][7] % 2 == 0,
+ X[2][1] % 2 == 0,
+ X[2][5] % 2 == 0,
+ X[4][3] % 2 == 0,
+ X[4][7] % 2 == 0,
+ X[6][1] % 2 == 0,
+ X[6][5] % 2 == 0,
+ X[8][3] % 2 == 0,
+ ]
+
+odds_c = [
+ X[1][2] % 2 == 1,
+ X[1][6] % 2 == 1,
+ X[3][0] % 2 == 1,
+ X[3][4] % 2 == 1,
+ X[3][8] % 2 == 1,
+ X[5][2] % 2 == 1,
+ X[5][6] % 2 == 1,
+ X[7][0] % 2 == 1,
+ X[7][4] % 2 == 1,
+ ]
+
+sums_c =[
+ X[0][5] + X[1][4] + X[2][3] + X[3][2] + X[4][1] + X[5][0] == 45,
+ X[1][0] + X[2][1] + X[3][2] + X[4][3] + X[5][4] + X[6][5] + X[7][6] + X[8][7] == 56,
+ X[3][0] + X[4][1] + X[5][2] + X[6][3] + X[7][4] + X[8][5] == 18,
+ X[0][6] + X[1][7] + X[2][8] == 11,
+ X[0][3] + X[1][4] + X[2][5] + X[3][5] + X[4][7] + X[5][8] == 24,
+ X[2][8] + X[3][7] + X[4][6] + X[5][5] + X[6][4] + X[7][3] + X[8][2] == 25,
+ X[6][8] + X[7][7] + X[8][6] == 8,
+ ]
+
+s = Solver()
+# s.add(sudoku_c + instance_c)
+# s.add(sudoku_c + evens_c + odds_c + sums_c)
+s.add(sudoku_c + evens_c + odds_c)
+if s.check() == sat:
+ m = s.model()
+ r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
+ for i in range(9) ]
+ print_matrix(r)
+else:
+ print("failed to solve")