Checkmate 30 kings, SAT constraints

theory.chess.check30.init.py

# Based on https://puzzling.stackexchange.com/questions/116750/checkmate-30-kings-with-rooks

def varchar(lit, seen=None):
    if seen:
        return {(True, True): "X", (True, False): "#", (False, True): ".", (False, False): "?"}[(lit in seen, -lit in seen)]
    else:
        v = slv.val(lit)
        if v is True: return "#"
        if v is False: return "."
        assert v is None
        if slv.resolvemerge(lit) != lit: return "/"
        if len(slv.lit_refs[lit]) + len(slv.lit_refs[-lit]) == 0 and len(slv.bclauses[lit]) == 0 and len(slv.bclauses[-lit]) == 0:
            return "*"
        return "?"
def one(slv, varset):
    varset = list(varset)
    slv.make_clause(varset)
    for i,a in enumerate(varset):
        for b in varset[:i]:
            slv.bclause(-a, -b)
class DummyCell:
    def __init__(self, slv, w, h):
        self.solver = slv
        self.boards = []
        for i in range(4 + 4 + 1):
            self.boards.append([slv.allocate_vars(w) for y in range(h)])
        wk, wr, bk, empty = self.boards[:4]
        rayb = self.boards[4:8]
        atk = self.boards[8]

        #slv.unit(wk[1][1])
        #slv.unit(wr[1][3])
        #slv.unit(wr[4][4])
        #slv.unit(wr[4][6])
        #for r in bk:
        #    for u in r: slv.unit(-u)
        #for r in wk:
        #    for u in r:
        #        if u not in slv.units: slv.unit(-u)
        #for r in wr:
        #    for u in r:
        #        if u not in slv.units: slv.unit(-u)
        #slv.make_clause(sum(wk, []))
        slv.make_clause(wk[0][0:4] + wk[1][1:4] + wk[2][2:4] + wk[3][3:4])
        #slv.make_clause(sum(bk, []))
        for y in range(h):
            for x in range(w):
                one(slv, [wk[y][x], bk[y][x], wr[y][x], empty[y][x]])
                for r in rayb: slv.bclause(-wr[y][x], r[y][x])
                for r in rayb: slv.make_clause([-r[y][x], empty[y][x], wr[y][x]])
                slv.bclause(-bk[y][x], atk[y][x])
                slv.propagate()
        for y in range(h):
            for x in range(w):
                esq = [-bk[y][x]]
                wksur = []
                for dy in (-1, 0, 1):
                    for dx in (-1, 0, 1):
                        if 0 <= x+dx < w and 0 <= y+dy < h:
                            if dx != 0 and dy != 0: slv.bclause(-bk[y][x], atk[y+dy][x+dx])
                            if (dy != 0 or dx != 0):
                                wksur += [wk[y+dy][x+dx]]
                                slv.bclause(-wk[y][x], atk[y+dy][x+dx])
                                slv.bclause(-wk[y][x], -bk[y+dy][x+dx])
                                slv.bclause(-wk[y][x], -bk[y+dy][x+dx])
                                esq += [atk[y+dy][x+dx], bk[y+dy][x+dx]]
                # esq
                print(x, y)
                self.pretty()
                slv.propagate()
                atkcl = [-atk[y][x]] + wksur
                for i, (dx, dy) in enumerate(((-1, 0), (1, 0), (0, -1), (0, 1))):
                    #slv.bclause(-rayb[i][y][x], -wk[y][x])
                    #slv.bclause(-rayb[i][y][x], -bk[y][x])
                    nx = x + dx
                    ny = y + dy
                    nnx = x - dx
                    nny = y - dy
                    if 0 <= nx < w and 0 <= ny < h:
                        if 0 <= nnx < w and 0 <= nny < h:
                            slv.make_clause([-bk[y][x], atk[ny][nx], rayb[i][nny][nnx]])
                        else:
                            slv.bclause(-bk[y][x], atk[ny][nx])
                        slv.bclause(-rayb[i^1][ny][nx], atk[y][x])
                        atkcl += [rayb[i^1][ny][nx]]
                        slv.make_clause([-rayb[i][y][x], -empty[ny][nx], rayb[i][ny][nx]])
                        slv.make_clause([-rayb[i^1][y][x], wr[y][x], rayb[i^1][ny][nx]])
                    else:
                        slv.make_clause([-rayb[i^1][y][x], wr[y][x]])
                slv.propagate()
                slv.make_clause(atkcl)
                slv.propagate()

    def pretty(self, seen=None):
        if seen is None:
            seen = {v if slv.val(v) else -v for v in range(1,len(slv.lit_refs)) if slv.val(v) is not None}
        for desc, b in zip("wKing wRook bKing empty rayL rayR rayU rayD atk".split(), self.boards):
            print("=== %s ===" % desc)
            format_grid(b, seen)

def format_grid(grid, val):
    for r in grid:
        out = ["%05d: "%r[0]]
        for u in r:
            out.append(varchar(u, val))
        print("".join(out))

slv = Solver()
cell = DummyCell(slv, 8, 8)
popbk = make_counter(slv, sum(cell.boards[2], []))
popwr = make_small_counter(slv, sum(cell.boards[1], []), 12)
popwk = make_small_counter(slv, sum(cell.boards[0], []), 6)
leximax_square(slv, cell.boards[0])
slv.unit(popbk[29])
slv.unit(-popbk[30]) # Exactly 30
slv.unit(popwr[10]) # 10 is known UNSAT
slv.unit(-popwr[11])