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

Question

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

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

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

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

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

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

Answer 1

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

• Р класс всех проблем, которые могут быть решены за полиномиальное время (то есть быстро).

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

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

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

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

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

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

Answer 2

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

Пример

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

Для чего он предназначен?

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

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