solve.py 2.7 KB

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576
  1. import itertools
  2. from graphviz import Digraph
  3. from chess_state import ChessState
  4. proof = Digraph(format='svg', node_attr={'shape': 'record'}, comment='Proof that chess domino is not possible')
  5. def state_id(index):
  6. return f'state{index}'
  7. class Solver:
  8. def __init__(self, board_size=8):
  9. self.board_size = board_size
  10. self.steps = 1
  11. self.starting_state = ChessState(board_size=board_size)
  12. max_steps = (board_size * board_size - 1) // 3
  13. self.states = [[] for _ in range(max_steps + 1)]
  14. self.states[0].append(self.starting_state)
  15. def solvable(self, state):
  16. if (self.board_size * self.board_size - 1) % 3 != 0:
  17. return False
  18. bricks_on_field = len(state.history())
  19. current_id = (bricks_on_field, len(self.states[bricks_on_field]) - 1)
  20. x, y = state.next_move()
  21. if x is None:
  22. return True # end of board
  23. for direction in ['right', 'down']:
  24. if state.possible(x, y, direction):
  25. next_state = state.put(x, y, direction)
  26. self.steps += 1
  27. found_symmetry = -1
  28. # look for symmetry
  29. for i, b in enumerate(self.states[bricks_on_field + 1]):
  30. if next_state.symmetric_to(b):
  31. print(f'found symmetry between states {current_id} and {(bricks_on_field, i)}')
  32. found_symmetry = i
  33. break
  34. # symmetry found
  35. if found_symmetry != -1:
  36. proof.edge(state_id(current_id),
  37. state_id(found_symmetry),
  38. label=f'put next brick facing {direction} at {(x,y)}')
  39. continue
  40. # pace next brick
  41. bricks_on_field += 1
  42. self.states[bricks_on_field].append(next_state)
  43. next_id = (bricks_on_field, len(self.states[bricks_on_field]) - 1)
  44. proof.edge(state_id(current_id),
  45. state_id(next_id),
  46. label=f'put next brick facing {direction} at {(x,y)}')
  47. proof.node(name=state_id(next_id), label=next_state.board_label())
  48. # try to solve the remaining board
  49. if self.solvable(next_state):
  50. return True
  51. return False
  52. if __name__ == '__main__':
  53. s = Solver(board_size=11)
  54. proof.node(name=state_id(0), label=s.starting_state.board_label())
  55. result = s.solvable(s.starting_state)
  56. print('solvable:', result)
  57. print('steps:', s.steps)
  58. print('states:', len(list(itertools.chain.from_iterable(s.states))))
  59. proof.render(f'img/proof.gv', view=False)