Пока я копался в материале для преподавания курса по решению SAT, я хотел выделить свое понимание кодирования SAT - процесса преобразования проблемы в проблему SAT - в форме, доступной для читателей с базовыми знаниями логики высказываний. Кроме того, вместо простого теоретического изложения, я хотел предоставить исполняемые примеры того, как хорошо известные проблемы информатики могут быть механически закодированы как задачи SAT и решены с помощью стандартных решателей SAT.

В этом контексте вот моя первая свалка о кодировании SAT :)

Удовлетворенность (SAT)

Для булевой формулы B, состоящей из набора пропозициональных переменных V и символов & (и), | (или), и! (отрицание) логических связок, проблема выполнимости (SAT) спрашивает: «Существует ли присвоение M истинных (T) или ложных (F) значений переменным V так, что B оценивается как истинное при M? ” Если такое присвоение M существует, то говорят, что оно удовлетворяет B, и это называется моделью B. Например, для формулы B = (a|b) & (!a|b) & (a|!b) ответ на соответствующую задачу SAT будет да и M = [a: T, b: T] - это модель B.

CNF

Логическая формула находится в Конъюнктивной нормальной форме (CNF), если формула представляет собой соединение (и) предложений, где каждое предложение предложение является дизъюнкцией (или) литералов и каждый literal - это либо пропозициональная переменная, либо отрицание пропозициональной переменной. Приведенная выше формула B является примером формулы CNF.

Было приложено много усилий для разработки методов и создания инструментов для решения задач SAT, то есть, чтобы определить, является ли формула CNF выполнимой, и определить модель формулы. Мы называем такие инструменты решателями SAT.

Кодирование SAT

Выполнимость интересна, поскольку любую проблему можно закодировать как формулу CNF, а решатель SAT можно использовать для решения соответствующей задачи SAT; конечно, возможность найти ответ - это отдельный разговор :)

Иллюстрация

Чтобы проиллюстрировать, как может работать такое кодирование, рассмотрим простую задачу сортировки трех чисел путем их кодирования как задачу SAT.

Мы представим эти три числа как целые переменные N1, N2 и N3. Поскольку имеется три числа, каждое число может встречаться в одной из трех позиций P1, P2 и P3 в отсортированном выводе, где число в позиции P1 меньше, чем число в позиции P2, меньше числа в позиции P3. Мы можем представить каждую из этих девяти возможностей пропозициональной переменной vNxPm, которая означает, что число Nx встречается в позиции Px в выходных данных.

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

  1. Каждое число Nx может встречаться только в одной позиции. В частности, для каждого Nx должно быть истинно ровно одно из vNxPm.
  2. Каждая позиция Pm может содержать только одно число. В частности, для каждого Pm должно быть истинным только одно из vNxPm.
  3. Если Nx встречается слева от Ny в выходных данных, то Nx должно быть меньше или равно Ny. В частности, если vNxPm и vNyPn истинны и m = n-1, то Nx ≤ Ny должно быть истинным.

Чтобы закодировать проблему как задачу SAT, мы должны перевести все эти ограничения в одну формулу CNF. Вот как мы можем это сделать.

  1. Первое ограничение может быть выражено как сочетание двух ограничений: Nx встречается по крайней мере в одной позиции и Nx встречается не более чем в одной позиции.
    Первое из этих двух ограничений может быть легко выражено в виде формулы CNF (vNxP1|vNxP2|vNxP3).
    Второе из этих двух ограничений не так просто выразить в виде формулы CNF, потому что ограничение преобразуется в
    i) если vNxP1, то и vNxP2, и vNxP3 должны быть ложными,
    ii) если vNxP2, то и vNxP3, и vNxP1 должны быть ложными, и
    iii) если vNxP3, то и vNxP1, и vNxP2 должны быть ложными .
    (i) может быть выражено в виде конъюнкции: если vNxP1, то vNxP2 ложно и если vNxP1, то vNxP3 ложно . В качестве логической формулы мы можем записать ее как
    (vNxP1 -> !vNxP2) & (vNxP1 -> !vNxP3).
    Поскольку A->B логически эквивалентно !A|B, мы можем переписать формулу как
    (!vNxP1|!vNxP2) & (!vNxP1|!vNxP3),, которая находится в CNF .
    Точно так же мы можем переписать (ii) и (iii) как
    (!vNxP2|!vNxP3) & (!vNxP3|!vNxP1)
    и
    (!vNxP3|!vNxP1) & (!vNxP3|!vNxP2) соответственно.
    Итак, для каждого Nx и для каждой эквивалентной круговой перестановки [Pm, Pn, Po] последовательности [P1, P2, P3] мы можем выразить первое ограничение в виде формулы CNF: (vNxPm|vNxPn|vNxPo) & (!vNxPm|!vNxPn) & (!vNxPm|!vNxPo). Следовательно, мы представим это ограничение с помощью 3x3x3 = 27 предложений.
  2. Поскольку ограничение 2 аналогично 1, для каждого Pm и для каждой эквивалентной круговой перестановки [Nx, Ny, Nz] последовательности [N1, N2, N3] мы можем выразить второе ограничение в виде формулы CNF:
    (vNxPm|vNyPm|vNzPm) & (!vNxPm|!vNyPm) & (!vNxPm|!vNzPm). Следовательно, мы представим это ограничение с помощью 3x3x3 = 27 предложений.
  3. Поскольку целочисленные операторы не могут встречаться в булевых формулах, мы должны перечислить возможности выражения третьего ограничения в виде булевой формулы. Поскольку рассматриваются только последовательные позиции (m = n-1), мы рассматриваем пары позиций (P1, P2) и (P2, P3).
    Кроме того, поскольку реляционные операторы не могут встречаться в булевых формулах, мы должны кодировать отношения как пропозициональные переменные: для каждой пары чисел (Nx, Ny), vNxLNy представляет Nx ≤Ny, т. е. если vNxLNy равно истина тогда и только тогда, когда Nx≤Ny.
    Теперь для каждой пары позиций (Pm, Pn) и пары чисел (Nx, Ny) мы можем выразить третье ограничение в виде логической формулы: ((vNxPm & vNyPn) -> vNxLNy). Как и раньше, мы можем переписать его как (!(vNxPm & vNyPn)|vNxLNy), что эквивалентно (!vNxPm|!vNyPn|vNxLNy). Следовательно, мы представим это ограничение с помощью 2x9 = 18 предложений.

В конце этого кодирования у нас будет в общей сложности 60 предложений, которые мы затем объединим в формулу CNF.

Независимо от сортируемых чисел результирующая формула всегда будет одинаковой. Итак, как только мы закодировали проблему в виде формулы CNF, мы можем повторно использовать формулу с незначительным расширением для решения различных экземпляров проблемы.

Например, чтобы отсортировать числа 10, 3 и 4 с использованием вышеуказанного кодирования, мы сопоставляем числа с N1, N2 и N3, мы определяем значение истинности vNxLNy для каждой пары чисел на основе сопоставления и расширяем CNF формула из кодировки с одним предложением, обозначающим значение истинности Nx≤Ny для каждой пары чисел (Nx, Ny), т.е. , если Nx≤Ny, то добавляется пункт vNxLNy; в противном случае добавляется пункт !vNxLNy. Мы передаем полученную формулу CNF решателю SAT и извлекаем результат из полученной модели: каждая переменная vNxPm, которой присвоено значение true в модели, интерпретируется как Nx, находящееся в позиции Pm в отсортированном выводе.

Это оптимальный размер?

Нет, но может быть.

Например, при кодировании ограничения 1 мы решили (в демонстрационных целях) сгенерировать (vNxPm|vNxPn|vNxPo) & (!vNxPm|!vNxPn) & (!vNxPm|!vNxPo) для каждого числа Nx и пары циклических перестановок. Это приведет к добавлению двух дубликатов предложения (vNxPm|vNxPn|vNxPo) из-за симметрии.

Другой пример: при кодировании ограничения 3, если значение истинности vNxLNy определено как истинное, то содержащее предложение не нужно генерировать, поскольку оно будет тривиально истинным. Если мы проигнорируем это наблюдение во время кодирования, мы можем создать бесполезные предложения. То же самое относится и к литералу! VNxLNy.

В зависимости от того, как мы формулируем ограничения и кодируем их как предложения, мы можем генерировать избыточные предложения и, возможно, избыточные пропозициональные переменные, которые могут раздувать окончательную формулу и могут способствовать увеличению времени выполнения. Итак, мы должны следить за избыточностью во время кодирования SAT.

Хорошо, может это действительно сработает?

Вот сценарий Groovy, который сортирует любые три заданных числа, кодируя задачу сортировки как задачу SAT и решая ее с помощью решателя Z3.

Размышления

Очевидно, это утомительный процесс для решения простой задачи сортировки трех чисел. Тот, которого следует избегать в реальных системах :)

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

Кроме того, как вы могли заметить, кодирование SAT в значительной степени зависит от перечисления возможностей и состояло всего из двух шагов:

  1. Выявление различных ограничений на вход проблемы, выход проблемы и отношения между входом и выходом.
  2. Выражение этих ограничений в терминах общих шаблонов ограничений, которые можно легко перевести в формулы CNF.

В этом смысле использование SAT-кодирования является более простым и более механическим подходом к решению проблем при условии: 1) идентификация требуемых ограничений проста и 2) существующие решатели SAT могут найти модели любой заданной формулы (если они существуют) за разумное время. Вы так не думаете?

Для вас

Подумайте, как можно расширить сортировщик для сортировки любых заданных n чисел.

Что дальше?

В следующий раз я перечислю общие шаблоны ограничений и их кодировки в виде формул CNF.