Что такое SAT и для чего это хорошо?

Недавно я увидел статью Reddit об использовании SAT для решения головоломки [1]. Это вызвало у меня очень интересные вещи об этом "SAT". Я прочитал статью в Википедии, но я хотел бы попросить кого-то из вас объяснить это мне в более простых условиях.

Что такое SAT и для чего это полезно? Может ли он использоваться для пересечения древовидной структуры? Для разбора текстов? Для разрыва строки [2]? Для упаковки в бутылки [3]? Это своего рода техника оптимизации?

Что касается соответствующей заметки, я прочитал, что NP против P - это выбор числа нулей в наборе, равного нулю, и проверки того, являются ли какие-то числа равными нулю, - это SAT, каким-то образом связанным с этим?

[1] http://www.reddit.com/r/programming/comments/pxpzd/solving_hexiom_really_fast_with_a_sat_solver/

[2] http://ru.wikipedia.org/wiki/Line_wrap

[3] http://ru.wikipedia.org/wiki/Bin_packing_problem

Ответ 1

SAT очень важен, потому что он NP-Complete. Чтобы понять, что это означает, вам нужно четкое представление о классах сложности. Вот краткое изложение:

P - класс всех задач, которые могут быть решены в полиномиальное время (т.е. быстро).
NP - это класс всех задач, для которых решение может быть проверено в полиномиальное время. Это означает, что решение данного решения выполняется быстро, но поиск одного из них обычно медленный (чаще всего экспоненциальное время). Если, конечно, проблема не в части P NP (как указано ниже, P является частью NP, как вы можете легко проверить).

Тогда есть набор проблем NP-Complete. Этот набор содержит всю проблему, которая является такой общей, вы можете решить эти Проблемы вместо другого из NP (это называется уменьшением проблемы на другую). Это означает, что вы можете превратить проблему из одного домена в другую проблему NP-Complete, получить ответ и преобразовать ответ.

Часто, однако, можно доказать, что проблема NP-Complete, но трансформации неясны для другой заданной проблемы.

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

Итак, да, SAT можно использовать для всех этих проблем, о которых вы говорите. Часто это не представляется возможным. Там, где это возможно, когда другой быстрый алгоритм не известен, например головоломка, которую вы упоминаете. В этом случае вам не нужно разрабатывать алгоритм для головоломки, но можете использовать любой из высоко оптимизированных SAT-Solvers, и вы получите разумный быстрый алгоритм для вашей головоломки.

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

Ответ 2

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

пример

предположим, что a, b и c являются булевыми переменными, и вы хотите знать, может ли им присваиваться значение, которое каким-то образом делает формулу (¬a ∨ b) ∧ (¬b ∨ c). Вы отправляете эту формулу к решатель SAT, и он вернет вам true. Решения SAT также часто дают вам действительное задание. В этом случае это назначение может быть a: false, b:false, c:false.

Для чего это можно использовать?

Я бы не использовал его, чтобы пересекать деревья, не разбирать текст и не разбивать строки. Однако вы можете использовать его при прохождении дерева, чтобы проверить, удовлетворены ли некоторые ограничения на дереве. Конечно, вы можете использовать его для упаковки бинов, хотя некоторые специализированные решатели CSP, вероятно, лучше справятся с такими проблемами.

В наши дни решатели SAT становятся все более распространенными, особенно в программном обеспечении, таком как менеджеры пакетов. Eclipse включает SAT4j для управления зависимостями между его плагинами. Другие приложения SAT обычно включают проверку модели, планирование приложений, конфигураторов, планирование и многие другие.