import itertools from graphviz import Digraph from chess_state import ChessState proof = Digraph(format='svg', node_attr={'shape': 'record'}, comment='Proof that chess domino is not possible') def state_id(index): return f'state{index}' class Solver: def __init__(self, board_size=8): self.board_size = board_size self.steps = 1 self.starting_state = ChessState(board_size=board_size) max_steps = (board_size * board_size - 1) // 3 self.states = [[] for _ in range(max_steps + 1)] self.states[0].append(self.starting_state) def solvable(self, state): if (self.board_size * self.board_size - 1) % 3 != 0: return False bricks_on_field = len(state.history()) current_id = (bricks_on_field, len(self.states[bricks_on_field]) - 1) x, y = state.next_move() if x is None: return True # end of board for direction in ['right', 'down']: if state.possible(x, y, direction): next_state = state.put(x, y, direction) self.steps += 1 found_symmetry = -1 # look for symmetry for i, b in enumerate(self.states[bricks_on_field + 1]): if next_state.symmetric_to(b): print(f'found symmetry between states {current_id} and {(bricks_on_field, i)}') found_symmetry = i break # symmetry found if found_symmetry != -1: proof.edge(state_id(current_id), state_id(found_symmetry), label=f'put next brick facing {direction} at {(x,y)}') continue # pace next brick bricks_on_field += 1 self.states[bricks_on_field].append(next_state) next_id = (bricks_on_field, len(self.states[bricks_on_field]) - 1) proof.edge(state_id(current_id), state_id(next_id), label=f'put next brick facing {direction} at {(x,y)}') proof.node(name=state_id(next_id), label=next_state.board_label()) # try to solve the remaining board if self.solvable(next_state): return True return False if __name__ == '__main__': s = Solver(board_size=11) proof.node(name=state_id(0), label=s.starting_state.board_label()) result = s.solvable(s.starting_state) print('solvable:', result) print('steps:', s.steps) print('states:', len(list(itertools.chain.from_iterable(s.states)))) proof.render(f'img/proof.gv', view=False)