Игра на основе SAT


Проблема логической выполнимости или SAT – самая известная проблема NP Complete. Это довольно легко понять, если вы знакомы с логикой логики, но теперь у нас есть простая игра, которая поможет вам действительно проникнуть в суть происходящего.

Проблема SAT хорошо известна. Возьмите длинное логическое выражение с k переменными и найдите, что k переменным присвоены значения true и false, что делает выражение истинным. Это может быть невозможно, но если это выражение считается удовлетворительным – отсюда и название проблемы.

Вариант решения проблемы состоит в том, чтобы просто решить, является ли данная формула выполнимой или нет.

Для k = 3 и больше задача SAT, как известно, является NP-полной.

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

«Полная» часть описания здесь, потому что, если вы можете решить задачу SAT за полиномиальное время, то все проблемы NP могут быть решены за полиномиальное время. То есть SAT – это представитель всей проблемы в NP.

Вы видите, что это важная проблема, но как мы можем ее лучше понять?

Оливье Байе из Университета Бургундии Franche-Comte изобрел красивую игру, которая эквивалентна задаче SAT.

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

Этот рисунок, взятый из статьи, показывает полную игру:

Порядок удаления токенов не имеет значения; имеют значение только начальное и конечное состояния.

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

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

Как это связано с проблемой SAT?

Каждая из коробок представляет собой логическое предложение. Каждый цвет является переменной, и квадрат соответствует истинному, а круглый – ложному.

Первоначальная конфигурация может быть прочитана как логическое выражение: квадрат – это положительная переменная, а круг – отрицательная. Итак, начальная конфигурация на рисунке выше соответствует:

(r или b или не p) и (не r или b или не p) и (r или не b или не p) и (не r или не b или не p) и (p или y) и (r или нет y) и (b или не y)

Проблема SAT состоит в том, чтобы найти присвоение true / false для r, b и p, чтобы каждое предложение было истинным – все они должны быть истинными, чтобы И для всех было истинным.

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

Если вы немного подумаете об этом, это приобретет смысл.

Если вы играете в игру, то начинаете понимать трудности задачи SAT.

Одно предупреждение: не сокращайте игру до двух цветов, просто чтобы посмотреть, как все работает, потому что проблема SAT для 2 переменных находится в P, а не в NP.

Теперь все, что нам нужно, – это чтобы кто-то реализовал ее в виде сетевой или мобильной игры, и мы все можем начать в нее играть.


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