Про булевскую выполнимость.
Поскольку у меня последнее время идиосинкразия к большим постам, буду конспективно.
SAT - задача на поиск решения логической формулы. Возвращает SAT (и решение), если нашлось, UNSAT - гарантировано нет решения и Intederminate - бились-бились, но за выделенное время решения не нашли.
Обычно формулу представляют в виде CNF - коньюнктивной нормальной формы. Это объединение через Логическое И Логических ИЛИ переменных и их отрицаний:
cnf ::= ;
cnf ::= disj /\ cnf;
disj ::= lit;
disj ::= lit \/ disj;
lit ::= var;
lit ::= !var;
Первый вариант поиска решения (Davis-Putnam) делал следующее - выбирал переменную и вычислял для всех дизъюнктов формулы Логическое И, выбирая их так, чтобы переменная схлопнулась: (!x|y)&(x|z) => y|z. Таким образом, переменная изымалась из рассмотрения, но увеличивалось количество дизъюнктов (и их размеры).
Далее была предложена оптимизация (Logemann-Loveland) - вместо создания множества дизъюнктов фиксируется значение переменной. В результате у нас может получиться так, что значения других переменных тоже фиксируются: x|y & !x => y. Это приводит к распространению значений логических переменных (unit propagation). В процессе распространения значений может возникнуть конфликт (одновременно присвоение x и !x переменной ч) и таким образом отсекается подмножество значений. Этот алгоритм разменивает пространство на время.
Оба алгоритма выше являются полными - они могут доказать и SAT, и UNSAT. Они перебирают значения, пока не достигнут решения (SAT) или не переберут все (UNSAT).
Про оптимизации я напишу позже. Из-за них современные SAT (с середины 90-х) решатели могут решать задачи с сотнями тысяч переменных и миллионами дизъюнктов. Для справки, первые DP решатели ограничивались десятком переменных и несколькими десятками дизъюнктов.
Но есть и неполные алгоритмы, стохастические. Они выбирают случайным образом присваивание для всех переменных, а потом стремятся уменьшить количество неудовлетворенных дизъюнктов, переключая значения переменных. Алгоритмы такого типа, хоть и быстро работают, не могут доказать UNSAT, поскольку не ведут учет просмотренных решений и, если не добавлять дополнительных проверок, могут крутиться на одном месте.
Что интересно, теоретически эти два направления сходятся.
В переборные алгоритмы класса DPLL добавляются перезапуски - после обнаружения некоторого условия текущий перебор отбрасывается и начинается "заново". Не совсем с той же точки, но с чистого листа. Все современные решатели ведут учет переменных и дизъюнктов, входивших в конфликты и на основе этой статистики производят выбор переменной для очередного шага. Но впервые перезапуски появились в стохастических алгоритмах, поскольку на одном месте они могли крутиться бесконечно долго. Проще было отбросить явно не сходящееся решение и начать заново.
В стохастические же алгоритмы добавлят учет переменных и дизъюнктов, что были не разрешены не так давно. Это позволяет улучшить скорость схождения.
SAT - задача на поиск решения логической формулы. Возвращает SAT (и решение), если нашлось, UNSAT - гарантировано нет решения и Intederminate - бились-бились, но за выделенное время решения не нашли.
Обычно формулу представляют в виде CNF - коньюнктивной нормальной формы. Это объединение через Логическое И Логических ИЛИ переменных и их отрицаний:
cnf ::= ;
cnf ::= disj /\ cnf;
disj ::= lit;
disj ::= lit \/ disj;
lit ::= var;
lit ::= !var;
Первый вариант поиска решения (Davis-Putnam) делал следующее - выбирал переменную и вычислял для всех дизъюнктов формулы Логическое И, выбирая их так, чтобы переменная схлопнулась: (!x|y)&(x|z) => y|z. Таким образом, переменная изымалась из рассмотрения, но увеличивалось количество дизъюнктов (и их размеры).
Далее была предложена оптимизация (Logemann-Loveland) - вместо создания множества дизъюнктов фиксируется значение переменной. В результате у нас может получиться так, что значения других переменных тоже фиксируются: x|y & !x => y. Это приводит к распространению значений логических переменных (unit propagation). В процессе распространения значений может возникнуть конфликт (одновременно присвоение x и !x переменной ч) и таким образом отсекается подмножество значений. Этот алгоритм разменивает пространство на время.
Оба алгоритма выше являются полными - они могут доказать и SAT, и UNSAT. Они перебирают значения, пока не достигнут решения (SAT) или не переберут все (UNSAT).
Про оптимизации я напишу позже. Из-за них современные SAT (с середины 90-х) решатели могут решать задачи с сотнями тысяч переменных и миллионами дизъюнктов. Для справки, первые DP решатели ограничивались десятком переменных и несколькими десятками дизъюнктов.
Но есть и неполные алгоритмы, стохастические. Они выбирают случайным образом присваивание для всех переменных, а потом стремятся уменьшить количество неудовлетворенных дизъюнктов, переключая значения переменных. Алгоритмы такого типа, хоть и быстро работают, не могут доказать UNSAT, поскольку не ведут учет просмотренных решений и, если не добавлять дополнительных проверок, могут крутиться на одном месте.
Что интересно, теоретически эти два направления сходятся.
В переборные алгоритмы класса DPLL добавляются перезапуски - после обнаружения некоторого условия текущий перебор отбрасывается и начинается "заново". Не совсем с той же точки, но с чистого листа. Все современные решатели ведут учет переменных и дизъюнктов, входивших в конфликты и на основе этой статистики производят выбор переменной для очередного шага. Но впервые перезапуски появились в стохастических алгоритмах, поскольку на одном месте они могли крутиться бесконечно долго. Проще было отбросить явно не сходящееся решение и начать заново.
В стохастические же алгоритмы добавлят учет переменных и дизъюнктов, что были не разрешены не так давно. Это позволяет улучшить скорость схождения.