Автор статьи Modern SAT solvers: fast, neat and underused утверждает, что SAT-солверы «преступно мало используются в нашей отрасли». [SAT — Boolean SATisfiability Solver, то есть солвер, способный находить присвоения, делающие истинными сложные булевы выражения. Более подробно я писал о них ранее.] Какое-то время назад я задался вопросом, почему: как получилось, что они настолько мощны, но ими никто не пользуется? Многие специалисты заявили, что причина в неудобстве кодирования SAT: они лучше предпочтут работать с инструментами, которые выполняют компиляцию в SAT.

Я вспомнил об этом, когда прочитал пост Райана Бергера о решении «задачи ферзей с LinkedIn» как задачи SAT.

Вкратце опишу задачу про ферзей (Queens). У нас есть сетка NxN, разделённая на N областей, и нам нужно разместить N ферзей так, чтобы в каждом столбце, строке и области находился ровно один. Ферзи могут находиться на одной диагонали, но не соседствовать по диагонали.

(Важное примечание: задача про ферзей с Linkedin — это вариация головоломки Star Battle, в которой количество звёзд, которые можно разместить в каждом столбце/строке/области разное для каждой головоломки, но обычно равно двум. Именно поэтому «ферзи» не съедают других, как в шахматах.)

Райан решил задачу, записав Queens в виде задачи SAT и выразив свойства вида «в строке 3 может быть ровно один ферзь» в виде большого количества булевых условий. Советую прочитать его пост, он очень любопытен. Неожиданным для меня оказалось то, что он использовал CVC5, то есть SMT-солвер. [Satisfiability Modulo Theories.] SMT-солверы более «высокоуровневые» по сравнению с SAT и способны работать с большим количеством типов данных, чем просто булевы переменные. Гораздо проще решить задачу на уровне SMT, чем на уровне SAT. Чтобы показать это, я набросал небольшое демо решения той же задачи на Z3 (с помощью Python API).

Вы можете сравнить мой полный код с SAT-решением Райана. Я не стал особо подчищать его (снова не хватило времени!), но ниже представлю краткое описание.

Код

from z3 import * # type: ignore
from itertools import combinations, chain, product
solver = Solver()
size = 9 # N

Подготовка и модули. size — это количество строк/столбцов/областей на доске, которое я ниже буду называть N.

# queens[n] = столбец ферзя в строке n
# по формулировке задачи, не в одной строке
queens = IntVector('q', size) 

SAT представляет позиции ферзей в виде N² булевых значений: q_00 означает, что ферзь находится в строке 0 и столбце 0, !q_05 означает, что ферзь не находится в строке 0, столбце 5 и так далее. В SMT мы можем закодировать это как N целых чисел: q_0 = 5 означает, что ферзь в строке 0 находится в столбце 5. Это мгновенно автоматически приводит в действие один класс ограничений: нам не нужны ограничения «в строке должен быть ровно один ферзь», потому что это встроено в определение queens!

(С моей стороны было ошибкой использовать индексацию с нуля, потому что в дальнейшем это сильно усложнило корректное кодирование областей.)

Для создания переменных [q_0, q_1, …] мы используем назначение Z3 IntVector(str, n), позволяющее одновременно создать n переменных.

solver.add([And(0 <= i, i < size) for i in queens])
# не в том же столбце
solver.add(Distinct(queens))

Сначала мы ограничиваем все целые числа интервалом [0, N), затем используем невероятно удобное ограничение Distinct, чтобы все целые числа принудительно имели разные значения. Это гарантирует, что в столбце будет максимум один ферзь, что по принципу Дирихле означает, что в каждом столбце будет ровно один ферзь.

# отсутствие диагонального соседства
for i in range(size-1):
    q1, q2 = queens[i], queens[i+1]
    solver.add(Abs(q1 - q2) != 1)

Одно из правил гласит, что ферзи не могут соседствовать. Исходя из других ограничений, мы уже знаем, что они не могут быть соседними по вертикали или горизонтали. Остаются диагонали. Нам нужно добавить лишь ограничение, по которому ни один ферзь не может находиться слева или справа внизу, то есть q_3 != q_2 ± 1. Верхние углы нам проверять не нужно, потому что если q_1 находится в верхнем левом углу от q_2, то q_2 находится в левом правом углу от q_1!

Так мы учли всё, кроме ограничения «один ферзь на область». Но с областями всё сложнее, и это вполне ожидаемо, ведь мы можем менять сложность игр про ферзей, меняя форму областей.

regions = {
        "purple": [(0, 0), (0, 1), (0, 2), (0, 3), (0, 4), (0, 5), (0, 6), (0, 7), (0, 8),
                   (1, 0), (2, 0), (3, 0), (4, 0), (5, 0), (6, 0), (7, 0), (8, 0),
                   (1, 1), (8, 1)],
        "red": [(1, 2), (2, 2), (2, 1), (3, 1), (4, 1), (5, 1), (6, 1), (6, 2), (7, 1), (7, 2), (8, 2), (8, 3),],
        # принцип понятен
        }

# Часть кода проверок пропущена, см. ниже

Область необходимо вводить вручную, что крайне неудобно.

(По ссылке дальше идёт код валидации. Так как он помешает объяснению модели, я расскажу о нём в следующем разделе).

for r in regions.values():
    solver.add(Or(
        *[queens[row] == col for (row, col) in r]
        ))

Наконец, у нас есть ограничение, связанное с областями. Простейший найденный мной способ сказать «в каждой области есть ровно один ферзь» оказался таким: «есть ферзь в области 1 и ферзь в области 2 и ферзь в области 3» и так далее. Тогда чтобы сообщить, что «есть ферзь в области purple», я напишу «q_0 = 0 OR q_0 = 1 OR … OR q_1 = 0» и так далее.

Зачем итеративно обходить каждую позицию в области вместо того, чтобы сделать что-то типа (0, q[0]) in r? Я пробовал так делать, но это выражение Z3 не поддерживает.

if solver.check() == sat:
    m = solver.model()
    print([(l, m[l]) for l in queens])

В конце мы выполняем решение и выводим позиции. Для моего примера задачи результат оказался таким:

[(q__0, 0), (q__1, 5), (q__2, 8), 
 (q__3, 2), (q__4, 7), (q__5, 4), 
 (q__6, 1), (q__7, 3), (q__8, 6)]

И это верное решение задачи с ферзями. Я не проводил бенчмарки времени решения, но могу представить, что оно существенно больше, чем у сырого SAT-солвера. Glucose крайне быстр.

Но даже всём при этом решать задачу при помощи SMT намного проще, чем при помощи SAT. Это отвечает на мой вопрос о том, почему люди предпочитают его, а не SAT.

Проверки

Выше я пропустил код проверок. Я точно знал, что совершу ошибку при кодировании region, а солвер не даст мне полезной информации о том, в чём я ошибся. В подобных случаях я добавляю небольшие тесты и проверки, чтобы отлавливать ошибки на ранних этапах, потому что солвер точно не будет их ловить!

all_squares = set(product(range(size), repeat=2))
def test_i_set_up_problem_right():
    assert all_squares == set(chain.from_iterable(regions.values()))

    for r1, r2 in combinations(regions.values(), 2):
        assert not set(r1) & set(r2), set(r1) & set(r2)

Первая проверка — это короткий тест того, что я не упустил ни одной клетки и не поместил случайно одну и ту же клетку в две области. Преобразование значений во множества сильно упрощает обе проверки. Честно говоря, я не знаю, почему сразу не использовал множества, они великолепны.

def render_regions():
    colormap = ["purple",  "red", "brown", "white", "green", "yellow", "orange", "blue", "pink"]
    board = [[0 for _ in range(size)] for _ in range(size)] 
    for (row, col) in all_squares:
        for color, region in regions.items():
            if (row, col) in region:
                board[row][col] = colormap.index(color)+1

    for row in board:
        print("".join(map(str, row)))

render_regions()

Вторая проверка выводит области. Она создаёт нечто подобное:

111111111
112333999
122439999
124437799
124666779
124467799
122467899
122555889
112258899

Я могу сравнить это с изображением доски, чтобы убедиться, что сделал всё правильно. Думаю, лучше бы было выводить эмодзи-квадраты, например ?.

Код обеих проверок не особо чистый, но это одноразовый код и он выполняет свою работу, так что пусть будет.