Skip to content

Instantly share code, notes, and snippets.

@regehr
Created December 6, 2018 04:30
Show Gist options
  • Save regehr/2b4ffd6585065573977b0f7847daf3b5 to your computer and use it in GitHub Desktop.
Save regehr/2b4ffd6585065573977b0f7847daf3b5 to your computer and use it in GitHub Desktop.
from z3 import *
n = 10
vars = []
def getConstraint(v, x, y):
if x < 0 or x >= n or y < 0 or y >= n:
return False
return v == (1 + vars[x][y])
s = SimpleSolver()
for x in range(0, n):
xl = []
for y in range(0, n):
v = Int('n' + str(x) + "x" + str(y))
s.add(v >= 1, v <= (n * n))
xl.append(v)
vars.append(xl)
for x in range(0, n):
for y in range(0, n):
v = vars[x][y]
c = v == 1
c = Or(c, getConstraint(v, x - 3, y))
c = Or(c, getConstraint(v, x + 3, y))
c = Or(c, getConstraint(v, x, y - 3))
c = Or(c, getConstraint(v, x, y + 3))
c = Or(c, getConstraint(v, x + 2, y + 2))
c = Or(c, getConstraint(v, x + 2, y - 2))
c = Or(c, getConstraint(v, x - 2, y + 2))
c = Or(c, getConstraint(v, x - 2, y - 2))
s.add(c)
s.add(Distinct([vars[x][y] for x in range(n) for y in range(n)]))
s.add(vars[0][0] == 1)
res = s.check()
print res
if res == sat:
m = s.model()
for x in range(0, n):
for y in range(0, n):
v = vars[x][y]
print repr(m[v]).rjust(3),
print
@tmyklebu
Copy link

tmyklebu commented Dec 9, 2018

Or just recursion:

#include <stdio.h>
#include <stdlib.h>
#include <string.h>

int adj[100][8], deg[100], mate[100], e[100][2], ne, ans[100], hits[100];

void dump() {
  for (int i = 0; i < 99; i++) hits[e[i][0]]++, hits[e[i][1]]++;
  for (int i = 0; i < 100; i++) if (hits[i] == 1) { ans[i] = 1; break; }
  for (int i = 0; i < 100; i++) for (int j = 0; j < 99; j++) {
    if (ans[e[j][0]] && !ans[e[j][1]]) ans[e[j][1]] = ans[e[j][0]]+1;
    if (ans[e[j][1]] && !ans[e[j][0]]) ans[e[j][0]] = ans[e[j][1]]+1;
  }
  for (int i = 0; i < 10; i++) {
    for (int j = 0; j < 10; j++)
      printf("%3i ", ans[10*i+j]);
    printf("\n");
  }
}

void doit(int v) {
  if (ne == 99) dump(), exit(0);
  if (mate[v] == -1) return doit(v+1);
  for (int i = 0; i < deg[v]; i++)
    if (mate[adj[v][i]] != -1 && mate[v] != adj[v][i]) {
      int w = adj[v][i];
      e[ne][0] = v; e[ne++][1] = w;
      int mv = mate[v], mw = mate[w];
      mate[v] = mate[w] = -1;
      mate[mv] = mw; mate[mw] = mv;
      doit(v);
      mate[v] = mv; mate[w] = mw;
      mate[mv] = v; mate[mw] = w;
      ne--;
    }
}

int main() {
  int ox[] = {3, 2, 0, 2}, oy[] = {0, 2, 3, -2};
  for (int i = 0; i < 10; i++) for (int j = 0; j < 10; j++)
    for (int k = 0; k < 4; k++) {
      int x = ox[k]+i, y = oy[k]+j, a = 10*i+j, b = 10*x+y;
      if (x >= 0 && y >= 0 && x < 10 && y < 10) adj[a][deg[a]++] = b;
    }
  for (int i = 0; i < 100; i++) mate[i] = i;
  doit(0);
}

It's pretty speedy:

tmyklebu@happyface:~$ time ./foo268
 72  25  16  65  35  52   6  92  37  50
 18  63  33  54   8  84  39  48  83  94
 31  56  71  26  15  66  36  51   5  91
 73  24  17  64  34  53   7  93  38  49
 19  62  32  55   9  85  40  47  82  95
 30  57  70  27  14  67  80  97   4  90
 74  23  12  59  78  44   2  88  43  99
 20  61  76  21  10  86  41  46  81  96
 29  58  69  28  13  68  79  98   3  89
 75  22  11  60  77  45   1  87  42 100

real    0m0.041s
user    0m0.040s
sys     0m0.000s

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment