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

Обозначим $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()

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

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