Проблема логической выполнимости - Boolean satisfiability problem

В логике и информатике , то булева задача выполнимости (иногда называемая пропозициональной проблема выполнимости и сокращенная выполнимость , SAT или B-SAT ) является проблема определения , если существует интерпретацию , что удовлетворяет заданную булева формулу . Другими словами, он спрашивает, могут ли переменные данной логической формулы быть последовательно заменены значениями ИСТИНА или ЛОЖЬ таким образом, чтобы формула оценивалась как ИСТИНА . В этом случае формула называется выполнимой . С другой стороны, если такое назначение не существует, то функция выражается формулой является значением FALSE для всех возможных назначений переменных и формула невыполнима . Например, формула « a AND NOT b » является выполнимой, потому что можно найти значения a  = TRUE и b  = FALSE, которые делают ( a AND NOT b ) = TRUE. В отличие от этого , « И НЕ » невыполнима.

SAT - первая задача, NP-завершенность которой доказана ; см. теорему Кука – Левина . Это означает, что все задачи класса сложности NP , который включает в себя широкий спектр задач естественного решения и оптимизации, труднее всего решить, как SAT. Не существует известного алгоритма, который бы эффективно решал каждую проблему SAT, и обычно считается, что такого алгоритма не существует; однако это убеждение не было доказано математически, и решение вопроса о том, имеет ли SAT алгоритм с полиномиальным временем , эквивалентно проблеме P против NP , которая является известной открытой проблемой в теории вычислений.

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

Основные определения и терминология

Логика высказываний формула , которая также называется логическое выражение , строится из переменных , операторов и ( совместно , также обозначаемой ∧) или ( дизъюнкции , ∨), НЕ ( отрицание , ¬), и круглые скобки. Формула считается выполнимой, если она может быть сделана ИСТИННОЙ путем присвоения соответствующих логических значений (т.е. ИСТИНА, ЛОЖЬ) ее переменным. Задача логической выполнимости (SAT) заключается в том, чтобы при наличии формулы проверить, выполнима ли она. Эта проблема решения имеет центральное значение во многих областях информатики , включая теоретическую информатику , теорию сложности , алгоритмику , криптографию и искусственный интеллект .

Существует несколько частных случаев проблемы булевой выполнимости, в которых требуется, чтобы формулы имели определенную структуру. Буквальным либо переменная, называется положительным буквальным , или отрицание переменной, называется отрицательной буквальным . Раздел является дизъюнкция литералов (или одного буквальным). Предложение называется предложением Horn, если оно содержит не более одного положительного литерала. Формула имеет конъюнктивную нормальную форму (CNF), если она является соединением предложений (или одним предложением). Например, x ₁ - положительный литерал, ¬ x ₂ - отрицательный литерал, x ₁ ∨ ¬ x ₂ - предложение. Формула ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ находится в конъюнктивной нормальной форме; его первое и третье предложения являются предложениями Хорна, а его второе предложение - нет. Формула выполняется при произвольном выборе x ₁  = FALSE, x ₂  = FALSE и x ₃ , поскольку (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x ₃ ) ∧ ¬FALSE оценивается как (FALSE ∨ TRUE) ∧ (ИСТИНА ∨ ЛОЖЬ ∨ x ₃ ) ∧ ИСТИНА и, в свою очередь, ИСТИНА ∧ ИСТИНА ∧ ИСТИНА (т.е. ИСТИНА). Напротив, формула CNF a ∧ ¬ a , состоящая из двух частей одного литерала, является неудовлетворительной, поскольку для a = TRUE или a = FALSE она принимает значение TRUE ∧ ¬TRUE (т. Е. FALSE) или FALSE ∧ ¬FALSE (т. Е. , снова FALSE) соответственно.

Для некоторых версий задачи SAT полезно определить понятие формулы обобщенной конъюнктивной нормальной формы , а именно. как конъюнкция произвольного числа обобщенных клозов , причем последнее имеет вид R ( l ₁ , ..., l _n ) для некоторой булевой функции R и (обычных) литералов l _i . Различные наборы разрешенных логических функций приводят к разным версиям проблемы. Например, R (¬ x , a , b ) является обобщенным предложением, а R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d , ¬ z ) является обобщенным конъюнктивная нормальная форма. Эта формула используется ниже , где R является тернарным оператором, который имеет значение ИСТИНА только тогда, когда имеет значение ровно один из его аргументов.

Используя законы булевой алгебры , любую формулу логики высказываний можно преобразовать в эквивалентную конъюнктивную нормальную форму, которая, однако, может быть экспоненциально длиннее. Например, преобразование формулы ( x ₁ ∧ y ₁ ) ∨ ( x ₂ ∧ y ₂ ) ∨ ... ∨ ( x _n ∧ y _n ) в конъюнктивную нормальную форму дает

( x ₁  ∨  x ₂  ∨… ∨  x _n ) ∧

( y ₁  ∨  x ₂  ∨… ∨  x _n ) ∧

( x ₁  ∨  y ₂  ∨… ∨  x _n ) ∧

( y ₁  ∨  y ₂  ∨… ∨  x _n ) ∧ ... ∧

( x ₁  ∨  x ₂  ∨… ∨  y _n ) ∧

( y ₁  ∨  x ₂  ∨… ∨  y _n ) ∧

( x ₁  ∨  y ₂  ∨… ∨  y _n ) ∧

( y ₁  ∨  y ₂  ∨… ∨  y _n ) ;

в то время как первая представляет собой дизъюнкцию n соединений 2 переменных, последняя состоит из 2 ⁿ частей n переменных.

Сложность и ограниченные версии

Неограниченная выполнимость (SAT)

SAT была первой известной NP-полной проблемой, что было доказано Стивеном Куком из Университета Торонто в 1971 году и независимо Леонидом Левиным из Национальной академии наук в 1973 году. До этого времени концепция NP-полной проблемы не применялась. даже существуют. Доказательство показывает, как каждая проблема решения в классе сложности NP может быть сведена к задаче SAT для формул CNF, иногда называемой CNFSAT . Полезное свойство редукции Кука состоит в том, что она сохраняет количество принимаемых ответов. Например, определение того, имеет ли данный граф 3-раскраску, - еще одна проблема в NP; если граф имеет 17 допустимых 3-раскрасок, формула SAT, полученная редукцией Кука – Левина, будет иметь 17 удовлетворительных назначений.

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

SAT тривиален, если формулы ограничены формулами в дизъюнктивной нормальной форме , то есть они являются дизъюнкцией конъюнкций литералов. Такая формула действительно выполнима тогда и только тогда, когда выполнима хотя бы одна из ее конъюнкций, а конъюнкция выполнима тогда и только тогда, когда она не содержит одновременно x и НЕ x для некоторой переменной x . Это можно проверить за линейное время. Более того, если они ограничены полной дизъюнктивной нормальной формой , в которой каждая переменная появляется ровно один раз в каждом соединении, они могут быть проверены в постоянное время (каждое соединение представляет собой одно удовлетворительное присвоение). Но для преобразования общей задачи SAT в дизъюнктивную нормальную форму могут потребоваться экспоненциальные время и пространство; например, поменяйте местами «∧» и «∨» в приведенном выше примере экспоненциального расширения для конъюнктивных нормальных форм.

3-выполнимость

Экземпляр 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 ₁ ∨ ⋯ ∨ l _n в конъюнкцию из n - 2 предложений.

( l ₁ ∨ l ₂ ∨ x ₂ ) ∧

(¬ x ₂ ∨ l ₃ ∨ x ₃ ) ∧

(¬ x ₃ ∨ l ₄ ∨ x ₄ ) ∧ ⋯ ∧

(¬ x _{n - 3} ∨ l _{n - 2} ∨ x _{n - 2} ) ∧

(¬ x _{n - 2} ∨ l _{n - 1} ∨ l _n )

где x ₂ , ⋯,  x _{n - 2} - новые переменные, нигде не встречающиеся. Хотя эти две формулы не являются логически эквивалентными , они равно выполнимы . Формула, полученная в результате преобразования всех клозов, не более чем в 3 раза длиннее оригинальной, т. Е. Рост длины полиномиален.

3-SAT - одна из 21 NP-полных задач Карпа , и она используется в качестве отправной точки для доказательства того, что другие проблемы также NP-трудны . Это делается путем полиномиального сокращения от 3-SAT к другой задаче. Примером проблемы, в которой использовался этот метод, является проблема клики : для данной формулы CNF, состоящей из c предложений, соответствующий граф состоит из вершины для каждого литерала и ребра между каждыми двумя непротиворечивыми литералами из разных предложений, ср. рисунок. Граф имеет c -клику тогда и только тогда, когда формула выполнима.

Существует простой рандомизированный алгоритм, предложенный Шёнингом (1999), который выполняется за время (4/3) ^n, где n - количество переменных в предложении 3-SAT, и с высокой вероятностью успешно принимает правильное решение для 3-SAT.

Гипотеза экспоненциального времени утверждает, что ни один алгоритм не может решить 3-SAT (или действительно k -SAT для любого ) за время exp ( o ( n )) (то есть существенно быстрее, чем экспоненциальный по n ). ${\ displaystyle k> 2}$

Селман, Митчелл и Левеск (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 ₁ ∨ ⋯ ∨ l _j с литералами j < k может быть дополнено фиксированными фиктивными переменными до l ₁ ∨ ⋯ ∨ l _j ∨ d _{j +1} ∨ ⋯ ∨ д _к . После заполнения всех предложений необходимо добавить 2 ^k -1 дополнительных предложений, чтобы гарантировать, что только d ₁ = ⋯ = d _k = FALSE может привести к удовлетворительному присваиванию. Поскольку k не зависит от длины формулы, дополнительные предложения приводят к постоянному увеличению длины. По той же причине не имеет значения, разрешены ли повторяющиеся литералы в предложениях, как в ¬ x ∨ ¬ y ∨ ¬ y .

Точно-1 3-выполнимость

Слева: сокращение Шефера предложения 3-SAT x ∨ y ∨ z . Результатом R будет ИСТИНА (1), если ровно один из его аргументов ИСТИНА, и ЛОЖЬ (0) в противном случае. Проверяются все 8 комбинаций значений x , y , z , по одной в строке. Новые переменные a , ..., f могут быть выбраны так, чтобы удовлетворять всем предложениям (ровно один зеленый аргумент для каждого R ) во всех строках, кроме первой, где x ∨ y ∨ z - ЛОЖЬ. Справа: более простая редукция с теми же свойствами.

Вариант задачи 3-выполнимости - это 3-SAT один из трех (также известный как 1-из-3-SAT и точно-1 3-SAT ). Учитывая конъюнктивную нормальную форму с тремя литералами на каждое предложение, проблема состоит в том, чтобы определить, существует ли такое присвоение истинности переменным, чтобы каждое предложение имело ровно один ИСТИННЫЙ литерал (и, следовательно, ровно два ЛОЖНЫХ литерала). Напротив, обычный 3-SAT требует, чтобы каждое предложение имело хотя бы один литерал TRUE. Формально, задача 3-SAT «один из трех» задается как обобщенная конъюнктивная нормальная форма со всеми обобщенными предложениями, использующими тернарный оператор R, который является ИСТИННЫМ, если только один из его аргументов является истинным. Когда все литералы формулы 3-SAT «один из трех» положительны, проблема выполнимости называется положительным 3-SAT «один из трех» .

Один-в-три 3-СБ, вместе с его положительным случаем, перечислен как NP-полной задачей «ОС4» в стандартной ссылке, Компьютеры и труднорешаемое: Руководство по теории NP-полнота по Майкл Р. Garey и Давида С. Джонсон . Один из трех 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 один из трех с 5 m разделами и n +6 m переменными. Другая редукция включает только четыре новых переменных и три предложения: R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d , ¬ z ), см. Рисунок (справа).

Не все равно 3-выполнимость

Другой вариант - проблема не-все-равной 3-выполнимости (также называемая NAE3SAT ). Учитывая конъюнктивную нормальную форму с тремя литералами на каждое предложение, проблема состоит в том, чтобы определить, существует ли такое присвоение переменным, что ни в одном предложении все три литерала имеют одинаковое значение истинности. Эта проблема тоже является NP-полной, даже если символы отрицания не допускаются, согласно теореме о дихотомии Шефера.

Линейный SAT

Формула 3-SAT называется Linear SAT ( LSAT ), если каждое предложение (рассматриваемое как набор литералов) пересекает не более одного другого предложения, и, более того, если два предложения пересекаются, то они имеют ровно один общий литерал. Формула LSAT может быть изображена как набор непересекающихся полузамкнутых интервалов на линии. Решение о том, является ли формула LSAT выполнимой или нет, является NP-полным.

2-выполнимость

SAT проще, если количество литералов в предложении ограничено максимум 2, и в этом случае проблема называется 2-SAT . Эта проблема может быть решена за полиномиальное время и фактически является полной для класса сложности NL . Если дополнительно все или операции в литералов изменяются на XOR операций, результат называется исключительным или 2-выполнимости , что является проблемой в комплекте для класса сложности SL = L .

Рог-выполнимость

Проблема определения выполнимости данной конъюнкции предложений Хорна называется выполнимостью по Хорну или HORN-SAT . Его можно решить за полиномиальное время с помощью одного шага алгоритма распространения единиц , который создает единственную минимальную модель набора предложений Horn (относительно набора литералов, присвоенных TRUE). Роговая выполнимость P-полная . Это можно рассматривать как версию P проблемы логической выполнимости. Кроме того, определение истинности количественных формул Хорна может быть выполнено за полиномиальное время.

Предложения Хорна интересны тем, что они могут выразить значение одной переменной из набора других переменных. В самом деле, одно такое предложение ¬ x ₁ ∨ ... ∨ ¬ x _n ∨ y может быть переписано как x ₁ ∧ ... ∧ x _n → y , то есть, если x ₁ , ..., x _n все ИСТИНА , тогда y также должно быть ИСТИНА.

Обобщением класса формул Хорна являются формулы переименовываемого Горна, которые представляют собой набор формул, которые можно преобразовать в форму Хорна, заменив некоторые переменные их соответствующим отрицанием. Например, ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ не является формулой Хорна, но может быть переименован в формулу Хорна ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ ¬ y ₃ ) ∧ ¬ x ₁ , введя y ₃ как отрицание x ₃ . Напротив, никакое переименование ( x ₁ ∨ ¬ x ₂ ∨ ¬ x ₃ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ приводит к формуле Хорна. Проверить наличие такой замены можно за линейное время; следовательно, выполнимость таких формул находится в P, поскольку ее можно решить, сначала выполнив эту замену, а затем проверив выполнимость полученной формулы Хорна.

Формула с двумя предложениями может быть неудовлетворенной (красный), 3-удовлетворенной (зеленый), xor-3-удовлетворенной (синий) или / и 1-из-3-удовлетворенной (желтой), в зависимости от количества ИСТИННЫХ буквальных значений в 1-е (гор.) и 2-е (верт.) предложения.

XOR-выполнимость

Другой особый случай - это класс проблем, в котором каждое предложение содержит операторы XOR (т.е. исключающее ИЛИ ), а не (простые) операторы ИЛИ. Это в P , поскольку формула XOR-SAT также может рассматриваться как система линейных уравнений по модулю 2 и может быть решена в кубическом времени методом исключения Гаусса ; см. пример на рамке. Это преобразование основано на родстве булевых алгебр и булевых колец , а также на том факте, что арифметика по модулю два образует конечное поле . Так как в XOR б XOR гр принимает значение TRUE , тогда и только тогда , когда ровно 1 или 3 члена { с , Ь , с } является TRUE, то каждое решение задачи 1-ин-3-SAT для данной формулы КНФА также является решение задачи 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 является частным случаем этой теоремы.

В следующей таблице приведены некоторые распространенные варианты SAT.

Расширения 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 (неявно) использует только ∃ кванторов. Если вместо этого разрешены только ∀ кванторов, получается так называемая проблема тавтологии , которая является ко-NP-полной . Если разрешены оба квантификатора, проблема называется проблемой квантифицированной логической формулы ( QBF ), которая, как можно показать, является PSPACE-полной . Широко распространено мнение, что PSPACE-полные задачи строго сложнее любых задач в NP, хотя это еще не доказано. Используя высокопараллельные P-системы , задачи QBF-SAT могут быть решены за линейное время.

Обычный тест SAT спрашивает, существует ли хотя бы одно присвоение переменной, которое делает формулу истинной. С количеством таких заданий справляются самые разные варианты:

• MAJ-SAT спрашивает, соответствует ли большинство заданий формуле ИСТИННОЙ. Для вероятностного класса PP он известен как полный .
• #SAT , проблема подсчета количества присвоений переменных, удовлетворяющих формуле, является проблемой подсчета, а не проблемой решения, и является # P-полной .
• UNIQUE SAT - это проблема определения того, имеет ли формула ровно одно присвоение. Это полное для США , в классе сложности , описывающей проблему разрешимы недетерминированное полиномиальное время машина Тьюринга , которая принимает , когда есть ровно один недетерминирован принимая путь и отбросы иначе.
• UNAMBIGUOUS-SAT - это название проблемы выполнимости, когда ввод ограничен формулами, имеющими не более одного удовлетворительного присваивания. Проблема также называется USAT . Алгоритм решения для UNAMBIGUOUS-SAT может демонстрировать любое поведение, включая бесконечный цикл, по формуле, имеющей несколько удовлетворительных назначений. Хотя эта проблема кажется проще, Valiant и Vazirani показали, что если существует практический алгоритм (т.е. алгоритм с рандомизированным полиномиальным временем ) для ее решения, то все проблемы в NP могут быть решены так же легко.
• MAX-SAT , проблема максимальной выполнимости , является обобщением SAT с помощью FNP . Требуется максимальное количество пунктов, которое может быть выполнено при любом назначении. У него есть эффективные алгоритмы аппроксимации , но его NP-трудно решить точно. Что еще хуже, это APX- полная, что означает, что для этой задачи не существует схемы полиномиального приближения (PTAS), если только P = NP.
• WMSAT - это задача нахождения присвоения минимального веса, которое удовлетворяет монотонной булевой формуле (то есть формуле без какого-либо отрицания). Вес пропозициональных переменных задается во входных данных задачи. Вес присвоения - это сумма весов истинных переменных. Эта проблема является NP-полной (см. Th. 1 из).

Другие обобщения включают выполнимость для логики первого и второго порядка , проблемы удовлетворения ограничений , целочисленное программирование 0-1 .

Самовосстановление

Задача SAT является самовосстанавливающейся , то есть каждый алгоритм, который правильно отвечает, если экземпляр SAT разрешим, можно использовать для поиска удовлетворительного назначения. Сначала задается вопрос о данной формуле Φ. Если ответ «нет», формула не выполняется. В противном случае задается вопрос о частично созданной формуле Φ { x ₁ = TRUE} , т. Е. Φ с первой переменной x _1, замененной на TRUE, и соответственно упрощается. Если ответ «да», то x ₁ = ИСТИНА, в противном случае x ₁ = ЛОЖЬ. Таким же образом впоследствии можно найти значения других переменных. Всего требуется n +1 запусков алгоритма, где n - количество различных переменных в Φ.

Это свойство самосводимости используется в нескольких теоремах теории сложности:

NP ⊆ P / poly ⇒ PH = Σ ₂   ( теорема Карпа – Липтона )

НП ⊆ БПП ⇒ НП = РП

P = NP ⇒ FP = FNP

Алгоритмы решения SAT

Поскольку задача SAT является NP-полной, для нее известны только алгоритмы с экспоненциальной сложностью наихудшего случая. Несмотря на это, в 2000-е годы были разработаны эффективные и масштабируемые алгоритмы для SAT, которые способствовали значительному прогрессу в нашей способности автоматически решать экземпляры проблем, включающие десятки тысяч переменных и миллионы ограничений (т. Е. Предложений). Примеры таких проблем в автоматизации электронного проектирования (EDA) включают в себя формальную проверку эквивалентности , проверку модели , формальную проверку на конвейерные микропроцессорах , автоматической генерации тестового шаблона , маршрутизации из FPGAs , планирования и задач планирования , и так далее. Механизм решения SAT теперь считается важным компонентом в наборе инструментов EDA .

Решающая программа DPLL SAT использует процедуру систематического поиска с возвратом для исследования (экспоненциального размера) пространства назначений переменных в поисках подходящих назначений. Базовая процедура поиска была предложена в двух основополагающих статьях в начале 1960-х (см. Ссылки ниже) и теперь обычно называется алгоритмом Дэвиса – Патнэма – Логеманна – Ловленда («DPLL» или «DLL»). Многие современные подходы к практическому решению SAT основаны на алгоритме DPLL и имеют ту же структуру. Часто они повышают эффективность только определенных классов проблем SAT, таких как экземпляры, которые появляются в промышленных приложениях или случайно сгенерированные экземпляры. Теоретически доказаны экспоненциальные нижние оценки для семейства алгоритмов DPLL.

Алгоритмы, не входящие в семейство DPLL, включают алгоритмы стохастического локального поиска . Одним из примеров является WalkSAT . Стохастические методы пытаются найти удовлетворительную интерпретацию, но не могут сделать вывод, что экземпляр SAT неудовлетворителен, в отличие от полных алгоритмов, таких как DPLL.

Напротив, рандомизированные алгоритмы, такие как алгоритм PPSZ Патури, Пудлака, Сакса и Зейна, устанавливают переменные в случайном порядке в соответствии с некоторыми эвристиками, например, с разрешением ограниченной ширины . Если эвристика не может найти правильную настройку, переменная назначается случайным образом. Алгоритм PPSZ имеет время работы в течение 3-SAT. Это была самая известная среда выполнения для этой проблемы до недавнего улучшения, сделанного Хансеном, Капланом, Замиром и Цвиком, которое имеет время выполнения для 3-SAT и в настоящее время является наиболее известной средой выполнения для k-SAT для всех значений k. В ситуации с множеством удовлетворительных назначений рандомизированный алгоритм Шёнинга имеет лучшую оценку. ${\ displaystyle O (1.308 ^ {n})}$${\ displaystyle O (1.307 ^ {n})}$

Современные решатели SAT (разработанные в 2000-х годах) бывают двух видов: «управляемые конфликтом» и «упреждающие». Оба подхода происходят от DPLL. Управляемые конфликтами решатели, такие как обучение на основе конфликта предложений (CDCL), дополняют базовый алгоритм поиска DPLL эффективным анализом конфликтов, обучением предложений, нехронологическим обратным отслеживанием (также известным как обратный переход ), а также блоком «два наблюдаемых литерала». распространение , адаптивное ветвление и случайные перезапуски. Эти «дополнения» к основному систематическому поиску, как было эмпирически показано, необходимы для обработки больших экземпляров SAT, которые возникают при автоматизации проектирования электроники (EDA). Хорошо известные реализации включают Chaff и GRASP . Упреждающие решатели особенно усилили редукцию (выходящую за рамки распространения единичных предложений) и эвристику, и они, как правило, сильнее, чем решатели, управляемые конфликтами, в жестких экземплярах (в то время как решатели, управляемые конфликтами, могут быть намного лучше в больших экземплярах, которые на самом деле имеют легкий экземпляр внутри).

Современные решатели SAT также оказывают значительное влияние на области проверки программного обеспечения, решения ограничений в искусственном интеллекте и исследования операций, среди прочего. Мощные решатели доступны в виде бесплатного программного обеспечения с открытым исходным кодом . В частности, управляемый конфликтом MiniSAT , который был относительно успешным на конкурсе SAT 2005 года , содержит всего около 600 строк кода. Современным решателем Parallel SAT является ManySAT. Он может обеспечить сверхлинейное ускорение на важных классах задач. Примером упреждающего решателя является march_dl , выигравший приз на конкурсе SAT 2007 года .

Определенные типы больших случайных выполнимых случаев SAT могут быть решены путем распространения обзора (SP). В частности, в приложениях для проектирования и проверки аппаратных средств выполнимость и другие логические свойства данной пропозициональной формулы иногда определяются на основе представления формулы в виде диаграммы двоичных решений (BDD).

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

Параллельное SAT-решение

Параллельные решатели SAT делятся на три категории: портфолио, алгоритмы « разделяй и властвуй» и параллельные алгоритмы локального поиска . В параллельных портфелях одновременно работают несколько различных решателей SAT. Каждый из них решает копию экземпляра SAT, тогда как алгоритмы «разделяй и властвуй» разделяют проблему между процессорами. Существуют разные подходы к распараллеливанию алгоритмов локального поиска.

Международный конкурс Solver СБ имеет параллельный трек , отражающий последние достижения в области параллельного решения SAT. В 2016, 2017 и 2018 годах тесты проводились в системе с общей памятью с 24 вычислительными ядрами , поэтому решатели, предназначенные для распределенной памяти или многоядерных процессоров, могли не работать .

Портфолио

Как правило, не существует решателя SAT, который лучше всех других решает все задачи SAT. Алгоритм может хорошо работать для проблемных экземпляров, с которыми борются другие, но будет хуже работать с другими экземплярами. Более того, для данного экземпляра SAT нет надежного способа предсказать, какой алгоритм решит этот экземпляр особенно быстро. Эти ограничения мотивируют подход параллельного портфеля. Портфолио - это набор разных алгоритмов или разных конфигураций одного и того же алгоритма. Все решатели в параллельном портфеле работают на разных процессорах для решения одной и той же проблемы. Если один решатель завершает свою работу, решатель портфеля сообщает, что проблема является выполнимой или неудовлетворительной в соответствии с этим одним решателем. Все остальные решатели прекращают работу. Диверсификация портфелей за счет включения различных решателей, каждое из которых хорошо работает с различным набором задач, повышает надежность решателя.

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

Одним из недостатков параллельных портфелей является количество повторяющейся работы. Если в последовательных решателях используется изучение предложений, совместное использование изученных предложений между параллельно работающими решателями может уменьшить дублирование работы и повысить производительность. Тем не менее, даже простое параллельное выполнение портфеля лучших решателей делает его конкурентоспособным. Примером такого решателя является PPfolio. Он был разработан для определения нижней границы производительности, которую должен обеспечить параллельный решатель SAT. Несмотря на большой объем повторяющейся работы из-за отсутствия оптимизаций, он хорошо работал на машине с общей памятью. HordeSat - это программа для решения параллельных портфелей для больших кластеров вычислительных узлов. В своей основе он использует по-разному настроенные экземпляры одного и того же последовательного решателя. В частности, для жестких экземпляров SAT HordeSat может обеспечивать линейное ускорение и, следовательно, значительно сокращать время работы.

В последние годы параллельные портфолио SAT-решателей доминировали в параллельных соревнованиях International SAT Solver Competitions . Известные примеры таких решателей включают Plingeling и безболезненные решения.

Разделяй и властвуй

В отличие от параллельных портфелей, параллельный принцип «разделяй и властвуй» пытается разделить пространство поиска между элементами обработки. Алгоритмы «разделяй и властвуй», такие как последовательный DPLL, уже применяют технику разделения пространства поиска, поэтому их расширение в сторону параллельного алгоритма является прямым. Однако из-за таких методов, как распространение единиц, после разделения частичные проблемы могут значительно отличаться по сложности. Таким образом, алгоритм DPLL обычно не обрабатывает каждую часть пространства поиска за одно и то же время, что приводит к сложной проблеме балансировки нагрузки .

Фаза куба для формулы . Эвристика принятия решений выбирает, какие переменные (кружки) назначить. После того, как эвристика отсечения решает прекратить дальнейшее ветвление, частичные проблемы (прямоугольники) решаются независимо с помощью CDCL.${\ displaystyle F}$

Из-за не хронологического поиска с возвратом распараллеливание обучения по конфликтным предложениям сложнее. Один из способов преодолеть это - парадигма Cube-and-Conquer . Предлагается решение в два этапа. На этапе «куб» Задача разбивается на многие тысячи, вплоть до миллионов разделов. Это делается упреждающим решателем, который находит набор частичных конфигураций, называемых «кубами». Куб также можно рассматривать как соединение подмножества переменных исходной формулы. В сочетании с формулой каждый кубик образует новую формулу. Эти формулы могут быть решены независимо и одновременно с помощью решателей, управляемых конфликтами. Поскольку дизъюнкция этих формул эквивалентна исходной формуле, проблема считается выполнимой, если выполняется одна из формул. Упреждающий решатель подходит для небольших, но сложных проблем, поэтому он используется для постепенного разделения проблемы на несколько подзадач. Эти подзадачи проще, но все же большие, что является идеальной формой для решателя, управляемого конфликтами. Более того, упреждающие решатели рассматривают всю проблему в целом, тогда как решающие программы, управляемые конфликтами, принимают решения на основе гораздо более локальной информации. В фазе куба задействованы три эвристики. Переменные в кубах выбираются эвристикой принятия решения. Эвристика направления решает, какое присвоение переменной (истинное или ложное) исследовать в первую очередь. В удовлетворительных проблемных случаях полезно сначала выбрать удовлетворительную ветвь. Эвристика отсечения решает, когда прекратить расширение куба и вместо этого перенаправить его последовательному решателю, управляемому конфликтами. Желательно, чтобы кубики были так же сложны для решения.

Treengeling - это пример параллельного решателя, который применяет парадигму Cube-and-Conquer. С момента своего появления в 2012 году он добился множества успехов на Международном конкурсе SAT Solver Competition . Cube-and-Conquer использовался для решения проблемы булевых пифагоровых троек .

Локальный поиск

Одна из стратегий параллельного алгоритма локального поиска для решения SAT - это одновременное выполнение нескольких переворотов переменных на разных процессорах. Другой - применить вышеупомянутый портфельный подход, однако совместное использование предложений невозможно, поскольку решатели локального поиска не создают предложения. В качестве альтернативы можно совместно использовать конфигурации, которые производятся локально. Эти конфигурации могут использоваться для управления производством новой начальной конфигурации, когда локальный решатель решает перезапустить свой поиск.

Смотрите также

• Неудовлетворительное ядро
• Выполнимость по модулю теорий
• Подсчет SAT
• Планар SAT
• Алгоритм Карлоффа-Цвика
• Выполнимость схемы

Примечания

использованная литература

Список литературы отсортирован по дате публикации:

внешние ссылки

• SAT Game - попробуйте сами решить задачу логической выполнимости

Формат задачи SAT

Проблема SAT часто описывается в формате DIMACS-CNF : входном файле, в котором каждая строка представляет собой единственную дизъюнкцию. Например, файл с двумя строками

1 -5 4 0
-1 5 3 4 0

представляет формулу «( x ₁ ∨ ¬ x ₅ ∨ x ₄ ) ∧ (¬ x ₁ ∨ x ₅ ∨ x ₃ ∨ x ₄ )».

Другой распространенный формат этой формулы - это 7-битное представление ASCII "(x1 | ~ x5 | x4) & (~ x1 | x5 | x3 | x4)".

• BCSAT - это инструмент, который преобразует входные файлы в удобочитаемом формате в формат DIMACS-CNF.

Онлайн-решатели SAT

• BoolSAT - решает формулы в формате DIMACS-CNF или в более удобном для человека формате: «a, а не b или a». Работает на сервере.
• Logictools - предоставляет различные решатели на JavaScript для обучения, сравнения и взлома. Работает в браузере.
• minisat-in-your-browser - решает формулы в формате DIMACS-CNF. Работает в браузере.
• SATRennesPA - решает формулы, написанные в удобной для пользователя форме. Работает на сервере.
• somerby.net/mack/logic - решает формулы, написанные в символьной логике. Работает в браузере.

Автономные решатели SAT

• MiniSAT - формат DIMACS-CNF и формат OPB для его сопутствующей программы решения псевдобулевых ограничений MiniSat +
• Линглинг - выиграл золотую медаль на соревнованиях SAT 2011 года.
  • PicoSAT - более ранний решатель из группы Lingeling.
• Sat4j - формат DIMACS-CNF. Доступен исходный код Java.
• Глюкоза - формат DIMACS-CNF.
• RSat - выиграл золотую медаль в конкурсе SAT 2007 года.
• UBCSAT . Поддерживает невзвешенные и взвешенные предложения в формате DIMACS-CNF. Исходный код C размещен на GitHub .
• CryptoMiniSat - выиграл золотую медаль в конкурсе SAT 2011 года. Исходный код C ++ размещен на GitHub . Пытается объединить многие полезные функции ядра MiniSat 2.0, PrecoSat ver 236 и Gluosis в один пакет, добавляя множество новых функций.
• Spear - поддерживает арифметику с битовыми векторами. Может использовать формат DIMACS-CNF или формат Spear .
  • HyperSAT - Создан для экспериментов с сокращением пространства поиска в B-кубах. Занял 3-е место в конкурсе SAT 2005 года. Более ранний и более медленный решатель от разработчиков Spear.
• BASolver
• АргоСАТ
• Fast SAT Solver - основан на генетических алгоритмах .
• zChaff - больше не поддерживается.
• BCSAT - удобочитаемый формат логической схемы (также преобразует этот формат в формат DIMACS-CNF и автоматически подключается к MiniSAT или zChaff).
• gini - язык SAT-решателя Go со связанными инструментами.
• gophersat - программа решения SAT на языке Go, которая также может справляться с псевдобулевыми задачами и проблемами MAXSAT.
• CLP (B) - логическое программирование с ограничениями, например SWI-Prolog .

SAT заявки

• WinSAT v2.04 : приложение SAT для Windows, созданное специально для исследователей.

Конференции

• Международная конференция по теории и приложениям проверки выполнимости

Публикации

• Журнал выполнимости, логического моделирования и вычислений
• Распространение обзора

Контрольные точки

• Принудительные удовлетворительные тесты SAT
• Тесты проверки программного обеспечения
• Тесты Fadi Aloul SAT

Решение SAT в целом:

• http://www.satlive.org
• http://www.satisfiability.org

Оценка решателей SAT

• Ежегодная оценка решателей SAT
• Результаты оценки SAT-решателей за 2008 год
• Международные соревнования SAT
• История

Дополнительная информация о SAT:

• SAT и MAX-SAT для непрофессионала
• SAT / SMT на примере

В эту статью включены материалы из колонки электронного информационного бюллетеня ACM SIGDA, подготовленной профессором Каремом Сакаллахом.
Оригинальный текст доступен здесь.