Что такое SAT и для чего он хорош? - PullRequest
12 голосов
/ 21 февраля 2012

Недавно я увидел статью 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://en.wikipedia.org/wiki/Line_wrap

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

Ответы [ 2 ]

8 голосов
/ 21 февраля 2012

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

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

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

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

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

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

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

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

6 голосов
/ 12 октября 2012

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

Пример

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

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

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

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

...