Войти
В логике и информатика, проблема логической выполнимости (иногда называемая проблема пропозициональной выполнимости и сокращенно УДОВЛЕТВОРЕНИЕ, SAT или B-SAT ) - это проблема определения, существует ли интерпретация, согласно которой удовлетворяет заданной Булевой формуле. Другими словами, он спрашивает, могут ли переменные данной логической формулы быть последовательно заменены значениями ИСТИНА или ЛОЖЬ таким образом, чтобы формула оценивалась как ИСТИНА. В этом случае формула называется выполнимой. С другой стороны, если такого присвоения не существует, функция, выраженная формулой, будет FALSE для всех возможных назначений переменных, и формула не выполнима. Например, формула «А И НЕ b» выполнима, потому что можно найти значения а = ИСТИНА и b = ЛОЖЬ, которые делают (а И НЕ b) = ИСТИНА. Напротив, «И-НЕ» невозможно выполнить.
SAT - первая проблема, которая оказалась NP-завершенной ; см. теорема Кука – Левина. Это означает, что все задачи в классе сложности NP, который включает широкий спектр естественных задач решения и оптимизации, в лучшем случае так же сложны, как и SAT. Не существует известного алгоритма, который эффективно решает каждую задачу SAT, и обычно считается, что такого алгоритма не существует; однако это убеждение не было доказано математически, и решение вопроса о том, имеет ли SAT алгоритм с полиномиальным временем, эквивалентно проблеме P по сравнению с NP, которая является известной открытой проблемой в теория вычислений.
Тем не менее, по состоянию на 2007 год эвристические SAT-алгоритмы способны решать примеры проблем, включающие десятки тысяч переменных и формул, состоящих из миллионов символов, что достаточно для многих практических задач SAT, например, из искусственный интеллект, схемотехника и автоматическое доказательство теорем.
A логика высказываний формула, также называемое логическим выражением, состоит из переменных, операторов AND (конъюнкция, также обозначается ∧), OR (дизъюнкция, ∨), NOT (отрицание, ¬) и круглые скобки. Формула считается выполнимой, если ее можно сделать ИСТИННОЙ, присвоив ее переменным соответствующие логические значения (то есть ИСТИНА, ЛОЖЬ). Задача логической выполнимости (SAT) состоит в том, чтобы при наличии формулы проверить, выполнима ли она. Эта проблема решения имеет центральное значение во многих областях информатики, включая теоретическую информатику, теорию сложности, алгоритмику., криптография и искусственный интеллект.
Существует несколько частных случаев проблемы логической выполнимости, в которых формулы должны иметь определенную структуру. Литерал - это либо переменная, называемая положительным литералом, либо отрицание переменной, называемое отрицательным литералом. Предложение - это дизъюнкция литералов (или одного литерала). Предложение называется Предложение Horn, если оно содержит не более одного положительного литерала. Формула находится в нормальной конъюнктивной форме (CNF), если она является соединением предложений (или одним предложением). Например, x 1 - положительный литерал, ¬x 2 - отрицательный литерал, x 1 ∨ ¬x 2 - это пункт. Формула (x 1 ∨ ¬x 2) ∧ (¬x 1 ∨ x 2 ∨ x 3) ∧ ¬x 1 находится в конъюнктивной нормальной форме; его первое и третье предложения являются предложениями Хорна, а его второе предложение - нет. Формула выполнима, если произвольно выбрать x 1 = FALSE, x 2 = FALSE и x 3, поскольку (FALSE ∨ ¬FALSE) ∧ (¬ ЛОЖЬ ∨ ЛОЖЬ ∨ x 3) ∧ ¬FALSE оценивается как (ЛОЖЬ ∨ ИСТИНА) ∧ (ИСТИНА ∨ ЛОЖЬ ∨ x 3) ∧ ИСТИНА и, в свою очередь, ИСТИНА ∧ ИСТИНА ∧ ИСТИНА (т.е. ИСТИНА). Напротив, формула CNF a ∧ ¬a, состоящая из двух частей одного литерала, является неудовлетворительной, поскольку для a = TRUE или a = FALSE она оценивается как TRUE ∧ ¬TRUE (т.е. FALSE) или FALSE ∧ ¬FALSE (т.е., снова FALSE) соответственно.
Для некоторых версий задачи SAT полезно определить понятие формулы обобщенной конъюнктивной нормальной формы, а именно. как соединение произвольного количества обобщенных предложений, причем последнее имеет форму R (l 1,..., l n) для некоторого логического оператора R и (обычных) литералов l я. Различные наборы допустимых логических операторов приводят к разным версиям проблемы. Например, R (¬x, a, b) является обобщенным предложением, а R (¬x, a, b) ∧ R (b, y, c) ∧ R (c, d, ¬z) является обобщенным конъюнктивная нормальная форма. Эта формула используется ниже, где R является тернарным оператором, который имеет значение ИСТИНА только тогда, когда равен ровно одному из его аргументов.
Используя законы булевой алгебры, каждая формула пропозициональной логики может быть преобразована в эквивалентную конъюнктивную нормальную форму, которая, однако, может быть экспоненциально длиннее. Например, преобразование формулы (x 1∧y1) ∨ (x 2∧y2) ∨... ∨ (x n∧yn) в конъюнктивную нормальную форму дает
в то время как первое представляет собой дизъюнкцию n конъюнкций двух переменных, второе состоит из 2 предложения от n переменных.
SAT была первой известной NP-полной проблемой, как доказал Стивен Кука в Университете Торонто в 1971 г. и независимо Леонидом Левином в Национальной академии наук в 1973 г. До этого времени концепция NP-полной проблемы даже не существовало. Доказательство показывает, как каждая проблема решения в классе сложности NP может быть сведена к задаче SAT для формул CNF, иногда называемой CNFSAT . Полезное свойство редукции Кука состоит в том, что она сохраняет количество принимаемых ответов. Например, определение того, имеет ли данный граф 3-раскраску, является другой проблемой в NP; если график имеет 17 допустимых 3-раскрасок, формула SAT, полученная редукцией Кука – Левина, будет иметь 17 удовлетворительных назначений.
NP-полнота относится только к времени выполнения в наихудших случаях. Многие случаи, возникающие в практических приложениях, можно решить гораздо быстрее. См. Алгоритмы решения SAT ниже.
SAT является тривиальным, если формулы ограничены формулами в дизъюнктивной нормальной форме, то есть они представляют собой дизъюнкцию конъюнкций литералов. Такая формула действительно выполнима тогда и только тогда, когда выполнима хотя бы одна из ее конъюнкций, а конъюнкция выполнима тогда и только тогда, когда она не содержит одновременно x и НЕ x для некоторой переменной x. Это можно проверить за линейное время. Более того, если они ограничены пребыванием в полной дизъюнктивной нормальной форме, в которой каждая переменная появляется ровно один раз в каждом соединении, они могут быть проверены в постоянное время (каждое соединение представляет одно удовлетворительное присвоение). Но для преобразования общей задачи SAT в дизъюнктивную нормальную форму могут потребоваться экспоненциальные время и пространство; для примера поменяйте местами «∧» и «<» в выше пример экспоненциального расширения для конъюнктивных нормальных форм.
Экземпляр 3-SAT (x ∨ x ∨ y) ∧ (¬x ∨ ¬y ∨ ¬y) ∧ (¬x ∨ y ∨ y) сокращен до проблема клики. Зеленые вершины образуют 3-клику и соответствуют удовлетворяющему назначению x = FALSE, y = TRUE. Подобно проблеме выполнимости для произвольных формул, определение выполнимости формулы в конъюнктивной нормальной форме, где каждое предложение ограничено большинство трех литералов также являются NP-полными; эта проблема называется 3-SAT, 3CNFSAT или 3-выполнимостью . Чтобы уменьшить проблему неограниченного SAT до 3-SAT, преобразуйте каждое предложение l 1 ∨ ⋯ ∨ l n в соединение n - 2 предложений
где x 2, ⋯, x n - 2 - новые переменные, не встречающиеся в других местах. Хотя эти две формулы не являются логически эквивалентны, они равновыполнимы. Формула, полученная в результате преобразования всех предложений, не более чем в 3 раза длиннее своей исходной, т. Е. Рост длины полиномиален.
3 -SAT - одна из 21 NP-полной проблемы Карпа, и она используется в качестве отправной точки для доказательства того, что другие проблемы также NP-трудны. Это делается полиномиальное сокращение от 3-SAT к другой задаче. Пример задачи, в которой этот метод имеет s - это проблема клики : для данной формулы CNF, состоящей из c предложений, соответствующий граф состоит из вершины для каждого литерала и ребра между каждыми двумя непротиворечивыми литералами из разных статей, ср. картина. Граф имеет c-клику тогда и только тогда, когда формула выполнима.
Существует простой рандомизированный алгоритм, разработанный Шёнингом (1999), который выполняется во времени (4/3), где n - количество переменных. в предложении 3-SAT и с высокой вероятностью преуспевает в правильном решении 3-SAT.
гипотеза экспоненциального времени утверждает, что ни один алгоритм не может решить 3-SAT (или действительно k-SAT для любого k>2) за время exp (o (n)) (т. е. существенно быстрее, чем экспоненциальное по n).
Селман, Митчелл и Левеск (1996) приводят эмпирические данные о сложности случайно сгенерированных формул 3-SAT в зависимости от их параметров размера. Сложность измеряется числом рекурсивных вызовов, сделанных алгоритмом DPLL.
3-выполнимость может быть обобщена до k-выполнимости (k-SAT, также k -CNF-SAT ), когда формулы в CNF рассматриваются с каждым предложением, содержащим до k литералов. Однако, поскольку для любого k ≥ 3 эта задача не может быть ни легче, чем 3-SAT, ни сложнее, чем SAT, а последние два являются NP-полными, поэтому k-SAT должна быть.
Некоторые авторы ограничивают k-SAT формулами CNF с ровно k литералами . Это также не приводит к другому классу сложности, поскольку каждое предложение l 1 ∨ ⋯ ∨ l j с j < k literals can be padded with fixed dummy variables to l1∨ ⋯ ∨ l j ∨ d j + 1 ∨ ⋯ ∨ d k. После заполнения всех предложений необходимо добавить 2-1 дополнительных предложения, чтобы гарантировать, что только d 1 = ⋯ = d k = FALSE может привести к удовлетворительному присваиванию. Поскольку k не зависит от длины формулы, дополнительные предложения приводят к постоянному увеличению длины. По той же причине не имеет значения, разрешены ли повторяющиеся литералы в предложениях, как в ¬x ∨ ¬y ∨ ¬y.
Слева: Шефер сокращение предложения 3-SAT x ∨ y ∨ z. Результатом R является ИСТИНА (1), если ровно один из его аргументов ИСТИНА, и ЛОЖЬ (0) в противном случае. Проверяются все 8 комбинаций значений x, y, z, по одной в строке. Новые переменные a,..., f могут быть выбраны так, чтобы удовлетворять всем предложениям (ровно один зеленый аргумент для каждого R) во всех строках, кроме первой, где x ∨ y ∨ z - ЛОЖЬ. Справа: Более простая редукция с теми же свойствами. Вариантом задачи 3-выполнимости является 3-SAT один-к-3 (также известный как 1-in-3-SAT и точно-1 3-SAT ). Учитывая конъюнктивную нормальную форму с тремя литералами на каждое предложение, проблема состоит в том, чтобы определить, существует ли истинное присвоение переменных, чтобы каждое предложение имело ровно один ИСТИННЫЙ литерал (и, следовательно, ровно два ЛОЖНЫХ литерала). Напротив, обычный 3-SAT требует, чтобы каждое предложение имело хотя бы один литерал TRUE. Формально, задача 3-SAT «один из трех» задается как обобщенная конъюнктивная нормальная форма со всеми обобщенными предложениями, использующими тернарный оператор R, который имеет значение ИСТИНА, если только один из его аргументов является истинным. Когда все литералы формулы 3-SAT один из трех положительны, проблема выполнимости называется положительным 3-SAT один из трех .
3-SAT один из трех вместе с положительным случай, указана как NP-полная проблема «LO4» в стандартном справочнике «Компьютеры и неразрешимость: Руководство по теории NP-полноты» Майклом Р. Гэри и Дэвидом С. Джонсоном. Томас Джером Шефер доказал, что один из трех 3-SAT является NP-полным как частный случай теоремы о дихотомии Шефера, которая утверждает, что любая проблема, обобщающая булеву выполнимость в определенный путь находится либо в классе P, либо является NP-полным.
Шефер дает конструкцию, позволяющую легко за полиномиальное время сократить 3-SAT до 3-SAT один из трех. Пусть «(x или y или z)» будет предложением в формуле 3CNF. Добавьте шесть новых логических переменных a, b, c, d, e и f, которые будут использоваться для имитации этого предложения, а не другого. Тогда формула R (x, a, d) ∧ R (y, b, d) ∧ R (a, b, e) ∧ R (c, d, f) ∧ R (z, c, FALSE) выполняется по формуле некоторая установка новых переменных тогда и только тогда, когда хотя бы одно из x, y или z имеет значение ИСТИНА, см. рисунок (слева). Таким образом, любой экземпляр 3-SAT с m разделами и n переменными может быть преобразован в равноудовлетворительный экземпляр 3-SAT один из трех с 5m разделами и n + 6m переменными. Другая редукция включает только четыре новых переменных и три клоза: R (¬x, a, b) ∧ R (b, y, c) ∧ R (c, d, ¬z), см. Рисунок (справа).
Другой вариант - это не все равно 3-выполнимость (также называемая NAE3SAT ). Учитывая конъюнктивную нормальную форму с тремя литералами на каждое предложение, проблема состоит в том, чтобы определить, существует ли такое присвоение переменным, что ни в одном предложении все три литерала имеют одинаковое значение истинности. Эта проблема тоже является NP-полной, даже если символы отрицания не допускаются, по теореме о дихотомии Шефера.
SAT легче, если количество литералов в предложении ограничено не более 2, и в этом случае проблема называется 2-SAT. Эта проблема может быть решена за полиномиальное время и фактически является полным для класса сложности NL. Если дополнительно все операции OR в литералах заменяются на операции XOR, результат называется выполнимостью исключающим или двойным образом, что является полной проблемой для класса сложности SL = L.
Проблема определения выполнимости данной совокупности предложений Хорна называется выполнимостью Хорна или HORN-SAT . Это может быть решено за полиномиальное время с помощью одного шага алгоритма распространения единиц, который создает единственную минимальную модель набора предложений Horn (относительно набора литералов, присвоенных TRUE). Роговая выполнимость P-полная. Это можно рассматривать как P версию проблемы логической выполнимости. Кроме того, определение истинности количественных формул Хорна может быть выполнено за полиномиальное время.
Предложения Horn интересны тем, что они могут выражать импликацию одной переменной из набора других переменных. Действительно, одно такое предложение ¬x 1 ∨... ∨ ¬x n ∨ y может быть переписано как x 1 ∧... ∧ x n → y, то есть, если x 1,..., x n все ИСТИНА, тогда y также должно быть ИСТИНА.
Обобщением класса формул Горна являются формулы переименовываемого Горна, которые представляют собой набор формул, которые могут быть помещены в форму Хорна путем замены некоторых переменных их соответствующим отрицанием. Например, (x 1 ∨ ¬x 2) ∧ (¬x 1 ∨ x 2 ∨ x 3) ∧ ¬x 1 не является формулой Хорна, но может быть переименован в формулу Хорна (x 1 ∨ ¬x 2) ∧ (¬ x 1 ∨ x 2 ∨ ¬y 3) ∧ ¬x 1 путем введения y 3 как отрицание из x 3. Напротив, нет переименования (x 1 ∨ ¬x 2 ∨ ¬x 3) ∧ (¬x 1 ∨ x 2 ∨ x 3) ∧ ¬x 1 приводит к формуле Хорна. Проверить наличие такой замены можно за линейное время; следовательно, выполнимость таких формул находится в P, поскольку ее можно решить, сначала выполнив эту замену, а затем проверив выполнимость полученной формулы Хорна.
 Формула с 2 предложениями может быть неудовлетворенной (красный), 3-удовлетворенной (зеленый), xor-3-удовлетворенной (синий) или / и удовлетворенной 1 из 3 (желтый), в зависимости от ИСТИНА- количество букв в первом (hor) и втором (vert) предложении. |
| Решение примера XOR-SAT. с помощью исключения Гаусса | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Другой особый случай - это класс проблем, где каждое предложение содержит XOR (т.е. исключающее или ), а не (простое) операторы OR. Это в P, поскольку формула XOR-SAT также может рассматриваться как система линейных уравнений по модулю 2 и может быть решена в кубическом времени с помощью исключения Гаусса ; пример см. на рамке. Это преобразование основано на родстве между булевыми алгебрами и булевыми кольцами и на том факте, что арифметика по модулю два формирует конечное поле. Так как XOR b XOR c оценивается как ИСТИНА тогда и только тогда, когда ровно 1 или 3 члена {a, b, c} истинны, каждое решение задачи 1-в-3-SAT для данной формулы CNF также является решением задачи XOR-3-SAT, и, в свою очередь, каждое решение XOR-3-SAT является решением 3-SAT, см. картина. Как следствие, для каждой формулы CNF можно решить задачу XOR-3-SAT, определенную этой формулой, и на основе результата сделать вывод, что проблема 3-SAT разрешима или что 1-из-3- Проблема SAT неразрешима.
При условии, что классы сложности P и NP не равны, ни 2-, ни Horn-, ни XOR-выполнимость не является NP-полной, в отличие от SAT.
Приведенные выше ограничения (CNF, 2CNF, 3CNF, Horn, XOR-SAT) ограничивают рассматриваемые формулы как соединения подформул; каждое ограничение устанавливает определенную форму для всех подформул: например, только двоичные предложения могут быть подформулами в 2CNF.
Теорема о дихотомии Шефера утверждает, что для любого ограничения на булевы операторы, которые могут быть использованы для формирования этих подформул, соответствующая проблема выполнимости находится в P или NP-полной. Принадлежность к P выполнимости формул 2CNF, Horn и XOR-SAT является частным случаем этой теоремы.
Расширение, которое приобрело значительную популярность с 2003 года, выполнимости по модулю теорий (SMT ), которые могут обогащать формулы CNF линейными ограничениями, массивами, всевозможными ограничениями, неинтерпретируемыми функциями и т. Д. Такие расширения обычно остаются NP-полными, но теперь доступны очень эффективные решатели, которые могут обрабатывать многие подобные ограничения.
Проблема выполнимости становится более сложной, если и «для всех» (∀ ), и «существует» (∃ ) кванторам разрешено связывать логические переменные. Пример такого выражения было бы ∀x ∀y ∃z (x ∨ y ∨ z) ∧ (¬x ∨ ¬y ∨ ¬z); это действительно, поскольку для всех значений x и y подходящее значение z может быть найденным, а именно z = TRUE, если x и y равны FALSE, и z = FALSE, иначе. SAT (неявно) использует только ∃ кванторов. Если вместо этого разрешены только ∀ квантификаторов, так называемый получается тавтология проблема, которая является co-NP-complete. Если разрешены оба квантора, проблема называется количественной проблемой логической формулы (QBF ), что может быть показано как PSPACE-complete. Широко распространено мнение, что PSPACE-полные задачи строго сложнее любых задач в NP, хотя это еще не доказано. Используя высокопараллельные системы P, задачи QBF-SAT могут быть решены за линейное время.
Обычный SAT спрашивает, есть ли хотя бы одно присвоение переменной, которое делает формулу истинной. Множество вариантов имеют дело с количеством таких назначений:
Другие обобщения включают выполнимость для первого - и логики второго порядка, проблемы удовлетворения ограничений, 0-1 целочисленное программирование.
Проблема SAT самовосстанавливающаяся, то есть каждый алгоритм, который правильно отвечает, если экземпляр SAT solvable можно использовать для поиска удовлетворительного задания. Сначала задается вопрос о данной формуле Φ. Если ответ «нет», формула невыполнима. В противном случае вопрос задается по частично приведенной формуле Φ {x1= TRUE}, то есть Φ с первой переменной x 1, замененной на TRUE, и соответственно упрощается. Если ответ «да», то x 1 = TRUE, иначе x 1 = FALSE. Таким же образом впоследствии можно найти значения других переменных. Всего требуется n + 1 запуск алгоритма, где n - количество различных переменных в Φ.
Это свойство самовосстановления используется в нескольких теоремах теории сложности:
Поскольку задача SAT является NP-полной, для нее известны только алгоритмы с экспоненциальной сложностью наихудшего случая. Несмотря на это, в 2000-х годах были разработаны эффективные и масштабируемые алгоритмы для SAT, которые способствовали значительному прогрессу в нашей способности автоматически решать экземпляры проблем, включающие десятки тысяч переменных и миллионы ограничений (то есть предложений). Примеры таких проблем в автоматизации проектирования электроники (EDA) включают в себя формальную проверку эквивалентности, проверку модели, формальную проверку из конвейеризованную микропроцессоры, автоматическая генерация тестовых таблиц, маршрутизация из FPGA, планирование и задачи планирования, и так далее. Механизм SAT-решения теперь считается важным компонентом в наборе инструментов EDA.
Решающая программа DPLL SAT использует процедуру систематического поиска с возвратом для исследования (экспоненциального размера) пространства назначений переменных в поисках подходящих назначений. Базовая процедура поиска была предложена в двух основополагающих статьях в начале 1960-х годов (см. Ссылки ниже) и теперь обычно называется алгоритм Дэвиса – Патнэма – Логеманна – Ловленда («DPLL» или «DLL»).. Многие современные подходы к практическому решению SAT основаны на алгоритме DPLL и имеют ту же структуру. Часто они повышают эффективность только определенных классов проблем SAT, таких как экземпляры, которые появляются в промышленных приложениях или случайно сгенерированные экземпляры. Теоретически экспоненциальные нижние границы были доказаны для семейства алгоритмов DPLL.
Алгоритмы, которые не являются частью семейства DPLL, включают в себя стохастические алгоритмы локального поиска. Один из примеров - WalkSAT. Стохастические методы пытаются найти удовлетворительную интерпретацию, но не могут сделать вывод о том, что экземпляр SAT является неудовлетворительным, в отличие от полных алгоритмов, таких как DPLL.
Напротив, рандомизированные алгоритмы, такие как алгоритм PPSZ Патури, Пудлака, Сакса, и Зейн устанавливает переменные в случайном порядке в соответствии с некоторыми эвристиками, например, с ограниченной шириной разрешением. Если эвристика не может найти правильную настройку, переменная назначается случайным образом. Алгоритм PPSZ имеет время выполнения 
Современные решатели SAT (разработанные в 2000-х) бывают двух видов: «управляемые конфликтом» и «упреждающие». Оба подхода происходят от DPLL. Управляемые конфликтами решатели, такие как изучение предложений на основе конфликтов (CDCL), дополняют базовый алгоритм поиска DPLL эффективным анализом конфликтов, изучением предложений, не- (он же обратный переход ), как а также адаптивное ветвление и случайные перезапуски. Эти «дополнения» к базовому систематическому поиску, как было эмпирически показано, необходимы для обработки больших экземпляров SAT, которые возникают в автоматизации проектирования электроники (EDA). Хорошо известные реализации включают Chaff и GRASP. Упреждающие решатели особенно усилили редукцию (выходящую за рамки распространения единичных предложений) и эвристику, и они, как правило, сильнее, чем решатели, управляемые конфликтами, в жестких экземплярах (в то время как решатели, управляемые конфликтами, могут быть намного лучше в больших экземплярах, которые действительно легкий экземпляр внутри).
Современные решатели SAT также оказывают значительное влияние на области проверки программного обеспечения, решения ограничений в искусственном интеллекте и исследования операций, среди прочего. Мощные решатели доступны в виде бесплатного программного обеспечения с открытым исходным кодом. В частности, управляемый конфликтом MiniSAT, который был относительно успешным на конкурсе 2005 SAT, содержит всего около 600 строк кода. Современный решатель Parallel SAT - ManySAT. Он может обеспечить сверхлинейное ускорение на важных классах задач. Примером для упреждающих решателей является march_dl, который выиграл приз на конкурсе 2007 SAT.
Некоторые типы больших случайных выполнимых экземпляров SAT могут быть решены с помощью (SP). В частности, в приложениях проектирование аппаратных средств и верификация, выполнимость и другие логические свойства данной пропозициональной формулы иногда определяются на основе представления формулы в виде диаграммы двоичных решений (BDD).
Почти все решатели SAT включают тайм-ауты, поэтому они завершают работу в разумное время, даже если не могут найти решение. Разные решатели SAT найдут разные примеры легкими или сложными, и некоторые из них преуспевают в доказательстве неудовлетворенности, а другие в поиске решений. Все это поведение можно увидеть в соревнованиях по решению SAT.
Параллельное Решатели SAT делятся на три категории: портфолио, разделяй и властвуй и параллельные алгоритмы локального поиска. В параллельных портфелях одновременно работают несколько различных решателей SAT. Каждый из них решает копию экземпляра SAT, тогда как алгоритмы «разделяй и властвуй» разделяют проблему между процессорами. Существуют разные подходы к распараллеливанию алгоритмов локального поиска.
Международный конкурс SAT Solver Competition имеет параллельную трассу, отражающую последние достижения в области параллельного решения SAT. В 2016, 2017 и 2018 годах тесты выполнялись в системе с общей памятью с 24 ядрами обработки, поэтому решатели предназначены для распределенной памяти или многоядерные процессоры могли не справиться.
Как правило, не существует решателя SAT, который лучше всех других решает все задачи SAT. Алгоритм может хорошо работать для проблемных экземпляров, с которыми другие борются, но хуже с другими экземплярами. Кроме того, для данного экземпляра SAT нет надежного способа предсказать, какой алгоритм решит этот экземпляр особенно быстро. Эти ограничения мотивируют подход параллельного портфеля. Портфель - это набор разных алгоритмов или разных конфигураций одного и того же алгоритма. Все решатели в параллельном портфеле работают на разных процессорах для решения одной и той же задачи. Если одна решающая программа завершается, решающая программа портфеля сообщает, что проблема является выполнимой или неудовлетворительной в соответствии с этим решателем. Все остальные решатели прекращают работу. Диверсификация портфелей за счет включения множества решателей, каждое из которых хорошо справляется с различным набором задач, повышает надежность решателя.
Многие решатели используют внутри себя генератор случайных чисел. Диверсификация их семян - простой способ диверсифицировать портфель. Другие стратегии диверсификации включают включение, отключение или диверсификацию определенных эвристик в последовательном решателе.
Одним из недостатков параллельных портфелей является количество повторяющейся работы. Если в последовательных решателях используется обучение предложений, совместное использование изученных предложений между параллельно работающими решателями может уменьшить дублирование работы и повысить производительность. Тем не менее, даже простой параллельный запуск портфеля лучших решателей делает его конкурентоспособным. Примером такого решателя является PPfolio. Он был разработан для определения нижней границы производительности, которую должен обеспечивать параллельный решатель SAT. Несмотря на большой объем повторяющейся работы из-за отсутствия оптимизаций, он хорошо работал на машине с общей памятью. HordeSat - это программа для решения параллельных портфелей для больших кластеров вычислительных узлов. В своей основе он использует по-разному настроенные экземпляры одного и того же последовательного решателя. В частности, для жестких экземпляров SAT HordeSat может обеспечить линейное ускорение и, следовательно, значительно сократить время работы.
В последние годы параллельные портфолио SAT-решателей доминируют в параллельном треке International SAT Solver Competitions. Яркие примеры таких решателей включают Plingeling и painless-mcomsps.
В отличие от параллельных портфелей, параллельный Divide-and-Conquer пытается разделить пространство поиска между обработками элементы. Алгоритмы разделения и владения, такие как последовательный DPLL, уже применяют технику разделения пространства поиска, поэтому их расширение в сторону параллельного алгоритма является прямым. Однако из-за таких методов, как распространение единиц, после разделения частичные проблемы могут значительно отличаться по сложности. Таким образом, алгоритм DPLL обычно не обрабатывает каждую часть пространства поиска за один и тот же промежуток времени, что приводит к сложной проблеме балансировки нагрузки.
Фаза куба для формулы 
. Эвристика принятия решений выбирает, какие переменные (кружки) назначить. После того, как эвристика отсечения решает прекратить дальнейшее ветвление, частичные проблемы (прямоугольники) решаются независимо с помощью CDCL. Из-за не хронологического поиска с возвратом распараллеливание обучения по конфликтным предложениям становится более трудным. Один из способов преодолеть это - парадигма. Предлагается решение в два этапа. На этапе «куб» Задача делится на многие тысячи, вплоть до миллионов разделов. Это делается упреждающим решателем, который находит набор частичных конфигураций, называемых «кубами». Куб также можно рассматривать как соединение подмножества переменных исходной формулы. В сочетании с формулой каждый кубик образует новую формулу. Эти формулы могут быть решены независимо и одновременно с помощью решателей, управляемых конфликтами. Поскольку дизъюнкция этих формулы эквивалентны исходной формуле, проблема считается выполнимой, если выполняется одна из формул. Упреждающий решатель подходит для небольших, но сложных проблем, поэтому он используется для постепенного разделения проблемы на несколько подзадач. Эти подзадачи проще, но все же большие, что является идеальной формой для решателя, управляемого конфликтами. Более того, упреждающие решатели рассматривают всю проблему, тогда как решающие программы, управляемые конфликтами, принимают решения на основе гораздо более локальной информации. В фазе куба задействованы три эвристики. Переменные в кубах выбираются эвристикой принятия решения. Эвристика направления решает, какое присвоение переменной (истинное или ложное) исследовать в первую очередь. В удовлетворительных проблемных случаях полезно сначала выбрать удовлетворительную ветвь. Эвристика отсечения решает, когда прекратить расширение куба и вместо этого перенаправить его последовательному решателю, управляемому конфликтами. Предпочтительно, кубики также сложны для решения.
Treengeling является примером параллельного решателя, который применяет парадигму Cube-and-Conquer. С момента своего появления в 2012 году он добился нескольких успехов на Международном конкурсе SAT Solver Competition. Cube-and-Conquer использовался для решения задачи логических пифагоровых троек.
Одна из стратегий параллельного алгоритма локального поиска для решения SAT - это попытка одновременного переворота нескольких переменных на разных процессорах. Другой - применить вышеупомянутый портфельный подход, однако совместное использование предложений невозможно, поскольку решатели локального поиска не создают предложения. В качестве альтернативы можно совместно использовать конфигурации, произведенные локально. Эти конфигурации могут использоваться для создания новой начальной конфигурации, когда локальный решатель решает перезапустить свой поиск.
Ссылки упорядочены по дате публикации:
 | Викискладе есть материалы, связанные с проблемой логической выполнимости. |
Часто описывается проблема SAT в формате DIMACS-CNF : входной файл, в котором каждая строка представляет одну дизъюнкцию. Например, файл с двумя строками
1-5 4 0-1 5 3 4 0
представляет формулу «(x 1 ∨ ¬x 5 ∨ x 4) ∧ (¬x 1 ∨ x 5 ∨ x 3 ∨ x 4) ".
Другим распространенным форматом этой формулы является 7-битное ASCII представление «(x1 | ~ x5 | x4) (~ x1 | x5 | x3 | x4)».
Решение SAT в целом:
Дополнительная информация о SAT:
В эту статью включены материалы из колонки электронного информационного бюллетеня ACM SIGDA , подготовленного проф. Карем Сакаллах. Исходный текст доступен здесь
