Ход в игре «крестики-нолики» с помощью SAT-солвера

В этом посте я расскажу, как свести (для учебных целей) задачу финального хода в игре «крестики-нолики» к проблеме выполнимости булевой формулы (КНФ).

Обозначим $x_{ij}$ = «в стоит X», $y_{ij}$ = «в стоит O». Составим КНФ, обозначающую возможность сделать ход «крестиками», чтобы они выиграли.

Воспользуемся SAT-солвером pycryptosat.

1) В одной и той же клетке не может одновременно находиться X и O.

$\bigwedge_{i,j} (\neg x_{ij} \vee \neg y_{ij})$

Код

for i in inds:     for j in inds:         add_clause([('X', i, j, '-'), ('O', i, j, '-')])

2) Укажем, какие клетки заняты.

$\left( \bigwedge_{\substack{i, j \\ (i, j) \text{ занята X}}} x_{ij} \right) \wedge \left( \bigwedge_{\substack{i, j \\ (i, j) \text{ занята O}}} y_{ij} \right)$

Код

for i in inds:     for j in inds:         if field[i][j] == 'X':             add_clause([('X', i, j, '+')])         elif field[i][j] == 'O':             add_clause([('O', i, j, '+')])

3) Ход X производится в одну клетку:

$\bigwedge_{\substack{i, j\\(i, j) \text{ не занята}}}\bigwedge_{\substack{k, l\\(k, l) \text{ не занята}\\(i, j) \neq (k, l)}}(\neg x_{ij} \vee \neg x_{kl})$

Эта формула получена перемножением импликаций $\left( x_{ij} \to \bigwedge_{kl} \neg x_{kl}\right)$ .

Код

for i in inds:     for j in inds:         if field[i][j] == '.':             for k in inds:                 for l in inds:                     if (i, j) != (k, l) and field[k][l] == '.':                         add_clause([('X', i, j, '-'), ('X', k, l, '-')])

4) В свободных клетках нет O.

$\bigwedge_{(i, j) \text{ не занята}} \neg y_{ij}$

Код

for i in inds:     for j in inds:         if field[i][j] == '.':             add_clause([('O', i, j, '-')])

5) Выигрыш, если три X стоят в одной горизонтали, вертикали или диагонали.

$\begin{multline}x_{11}x_{12}x_{13} \vee x_{21}x_{22}x_{23} \vee x_{31}x_{32}x_{33} \vee\\ \vee x_{11}x_{12}x_{13} \vee x_{12}x_{22}x_{32} \vee x_{13}x_{23}x_{33} \vee\\ \vee x_{11}x_{22}x_{23} \vee x_{13}x_{22}x_{31}\end{multline}$

Автоматизируем перевод этой формулы к КНФ, применив распределительный закон.

Код

# Автоматически приведем условие выигрыша из ДНФ к КНФ dnf = [[(1, 1), (1, 2), (1, 3)], [(2, 1), (2, 2), (2, 3)], [(3, 1), (3, 2), (3, 3)],        [(1, 1), (1, 2), (1, 3)], [(1, 2), (2, 2), (3, 2)], [(1, 3), (2, 3), (3, 3)],        [(1, 1), (2, 2), (3, 3)], [(1, 3), (2, 2), (3, 1)]] dnf_len = len(dnf) # генерируем кортежи длины 8 из элементов 0, 1, 2 for seq in itertools.product([0, 1, 2], repeat=dnf_len):     clause = []     for p in range(dnf_len):         i, j = dnf[p][seq[p]]         clause.append(('X', i, j, '+'))     add_clause(clause)

Код примера

from pycryptosat import Solver import itertools   s = Solver()   # индекс переменной x_ij # i, j = 1, 2, 3 # индекс = 1..9 def vind(s, i, j):     assert(s == 'X' or s == 'O')     ind = (i - 1) * 3 + j     if s == 'O':         ind += 9     return ind   # добавить дизъюнкт к КНФ # vlist - список пар (i, j) def add_clause(vlist):     l = []     for p, i, j, r in vlist:         if r == '+':             l.append(vind(p, i, j))         elif r == '-':             l.append(-vind(p, i, j))         else:             raise ValueError("+ or - expected")     s.add_clause(l)   inds = range(1, 4)  # индексы клеток  # инициализация игрового поля field = [['.' for _ in range(0, 4)] for _ in range(0, 4)]  # игровая ситуация field[1][1] = 'X' field[1][3] = 'O' field[2][1] = 'O' field[3][3] = 'X'  # вывод поля for i in inds:     for j in inds:         print(field[i][j], end='')     print()  # 1. В одной и той же клетке не может одновременно находиться X и O for i in inds:     for j in inds:         add_clause([('X', i, j, '-'), ('O', i, j, '-')])  # 2. Укажем, какие клетки заняты for i in inds:     for j in inds:         if field[i][j] == 'X':             add_clause([('X', i, j, '+')])         elif field[i][j] == 'O':             add_clause([('O', i, j, '+')])  # 3. Ход X производится в одну клетку for i in inds:     for j in inds:         if field[i][j] == '.':             for k in inds:                 for l in inds:                     if (i, j) != (k, l) and field[k][l] == '.':                         add_clause([('X', i, j, '-'), ('X', k, l, '-')])  # 4. В свободных клетках нет O for i in inds:     for j in inds:         if field[i][j] == '.':             add_clause([('O', i, j, '-')])  # 5. Выигрыш, если три X стоят в одной горизонтали, вертикали или диагонали  # Автоматически приведем условие выигрыша из ДНФ к КНФ dnf = [[(1, 1), (1, 2), (1, 3)], [(2, 1), (2, 2), (2, 3)], [(3, 1), (3, 2), (3, 3)],        [(1, 1), (1, 2), (1, 3)], [(1, 2), (2, 2), (3, 2)], [(1, 3), (2, 3), (3, 3)],        [(1, 1), (2, 2), (3, 3)], [(1, 3), (2, 2), (3, 1)]] dnf_len = len(dnf) # генерируем кортежи длины 8 из элементов 0, 1, 2 for seq in itertools.product([0, 1, 2], repeat=dnf_len):     clause = []     for p in range(dnf_len):         i, j = dnf[p][seq[p]]         clause.append(('X', i, j, '+'))     add_clause(clause)   sat, solution = s.solve() #print(sat) #print(solution)  if not sat:     print('Нет решения') else:     new_field = [['.' for _ in range(0, 4)] for _ in range(0, 4)]     for i in inds:         for j in inds:             if solution[vind('X', i, j)]:                 new_field[i][j] = 'X'             elif solution[vind('O', i, j)]:                 new_field[i][j] = 'O'      # вывод поля     print("Решение:")     for i in inds:         for j in inds:             print(new_field[i][j], end='')         print()

Спасибо за просмотр. Буду рад ответить на вопросы.

ссылка на оригинал статьи https://habr.com/ru/articles/857352/

Ход в игре «крестики-нолики» с помощью SAT-солвера

Комментарии

Добавить комментарий Отменить ответ