В логике и информатике проблема булевой выполнимости (иногда называемая проблемой пропозициональной выполнимости и сокращенно ВЫПОЛНЯЕМОСТЬ , SAT или B-SAT ) — это проблема определения, существует ли интерпретация , удовлетворяющая данной булевой формуле . Другими словами, он спрашивает, могут ли переменные данной логической формулы быть последовательно заменены значениями ИСТИНА или ЛОЖЬ таким образом, чтобы формула имела значение ИСТИНА. В этом случае формула называется выполнимой . С другой стороны, если такого присвоения не существует, функция, выраженная формулой, является ЛОЖНОЙ для всех возможных присвоений переменных, и формула является невыполнимой . Например, формула « a AND NOT b » выполнима, поскольку можно найти значения a = TRUE и b = FALSE, которые делают ( a AND NOT b ) = TRUE. Напротив, выражение « А И НЕ а » невыполнимо.
SAT — первая задача, NP-полнота которой была доказана ; см. теорему Кука – Левина . Это означает, что все задачи класса сложности NP , который включает в себя широкий спектр задач естественного решения и оптимизации, в лучшем случае так же сложны для решения, как и SAT. Не существует известного алгоритма, который эффективно решает каждую задачу SAT, и обычно считается, что такого алгоритма не существует; однако это убеждение не было доказано математически, и решение вопроса о том, имеет ли SAT алгоритм с полиномиальным временем, эквивалентно проблеме P и NP , которая является известной открытой проблемой в теории вычислений.
Тем не менее, по состоянию на 2007 год эвристические SAT-алгоритмы способны решать экземпляры задач, включающие десятки тысяч переменных и формулы, состоящие из миллионов символов, [1] чего достаточно для многих практических задач SAT, например, в области искусственного интеллекта и проектирования схем. , [2] и автоматическое доказательство теорем .
Формула пропозициональной логики , также называемая логическим выражением , строится из переменных , операторов И ( конъюнкция , также обозначается ∧), ИЛИ ( дизъюнкция , ∨), НЕ ( отрицание , ¬) и круглых скобок. Формула считается выполнимой, если ее можно сделать ИСТИНОЙ путем присвоения ее переменным соответствующих логических значений (т. е. ИСТИНА, ЛОЖЬ). Задача булевой выполнимости (SAT) заключается в том, чтобы по заданной формуле проверить, выполнима ли она. Эта проблема решения имеет центральное значение во многих областях информатики , включая теоретическую информатику , теорию сложности , [3] [4] алгоритмику , криптографию [5] [6] и искусственный интеллект . [7] [ необходимы дополнительные ссылки ]
Литерал — это либо переменная (в этом случае он называется положительным литералом ), либо отрицание переменной (называемое отрицательным литералом ). Предложение — это дизъюнкция литералов (или один литерал). Предложение называется предложением Хорна , если оно содержит не более одного положительного литерала. Формула находится в конъюнктивной нормальной форме (КНФ), если она представляет собой соединение предложений (или одно предложение).
Например, 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) ∧ (¬FALSE ∨ FALSE ∨ x 3 ) ∧ ¬FALSE дает (FALSE ∨ TRUE) ∧ (ИСТИНА ∨ ЛОЖЬ ∨ x 3 ) ∧ ИСТИНА и, в свою очередь, к ИСТИНА ∧ ИСТИНА ∧ ИСТИНА (т. е. к ИСТИНА). Напротив, формула КНФ a ∧ ¬ a , состоящая из двух предложений одного литерала, невыполнима, поскольку для a =TRUE или a =FALSE она оценивается как TRUE ∧ ¬TRUE (т. е. FALSE) или FALSE ∧ ¬FALSE (т. е. , снова ЛОЖЬ), соответственно.
Для некоторых версий задачи SAT полезно определить понятие обобщенной формулы конъюнктивной нормальной формы , а именно. как соединение произвольного числа обобщенных предложений , причем последнее имеет форму R ( l 1 ,..., l n ) для некоторой булевой функции R и (обычных) литералов l i . Различные наборы разрешенных логических функций приводят к разным версиям проблемы. Например, R (¬ x , a , b ) является обобщенным предложением, а R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d ,¬ z ) является обобщенным предложением. конъюнктивная нормальная форма. Эта формула используется ниже, где R — это тернарный оператор, который имеет значение ИСТИНА только тогда, когда один из его аргументов является истинным.
Используя законы булевой алгебры , каждую формулу логики высказываний можно преобразовать в эквивалентную конъюнктивную нормальную форму, которая, однако, может быть экспоненциально длиннее. Например, преобразование формулы ( x 1 ∧ y 1 ) ∨ ( x 2 ∧ y 2 ) ∨ ... ∨ ( x n ∧ y n ) в конъюнктивную нормальную форму дает
в то время как первый представляет собой дизъюнкцию n конъюнкций по 2 переменных, второй состоит из 2 n предложений по n переменных.
Однако с помощью преобразования Цейтина мы можем найти эквивыполнимую формулу конъюнктивной нормальной формы с длиной, линейной по размеру исходной формулы пропозициональной логики.
SAT была первой известной NP-полной задачей, как доказал Стивен Кук из Университета Торонто в 1971 году [8] и независимо Леонид Левин из Российской академии наук в 1973 году . [9] До этого времени концепция NP-полной проблемы даже не существовало. Доказательство показывает, как любую проблему принятия решения в классе сложности NP можно свести к задаче SAT для формул CNF [примечание 1] , иногда называемой CNFSAT . Полезным свойством сокращения Кука является то, что оно сохраняет количество принимаемых ответов. Например, еще одна проблема в NP — решить, имеет ли данный граф 3-раскраску ; если граф имеет 17 допустимых трехцветных раскрасок, формула SAT, полученная с помощью сокращения Кука – Левина, будет иметь 17 удовлетворяющих назначений.
NP-полнота относится только к времени выполнения экземпляров наихудшего случая. Многие случаи, возникающие в практических приложениях, можно решить гораздо быстрее. См. Алгоритмы решения SAT ниже.
Как и проблема выполнимости произвольных формул, определение выполнимости формулы в конъюнктивной нормальной форме, где каждое предложение ограничено не более чем тремя литералами, также является NP-полным; эта проблема называется 3-SAT , 3CNFSAT или 3-выполнимостью . Чтобы свести неограниченную задачу SAT к 3-SAT, преобразуйте каждое предложение l 1 ∨ ⋯ ∨ l n в конъюнкцию из n - 2 предложений .
где x 2 , ⋯ , x n − 2 — свежие переменные, больше нигде не встречающиеся. Хотя эти две формулы логически не эквивалентны , они равновыполнимы . Формула, полученная в результате преобразования всех предложений, имеет длину не более чем в 3 раза, т. е. рост длины является полиномиальным. [10]
3-SAT — одна из 21 NP-полной задачи Карпа , и она используется в качестве отправной точки для доказательства того, что другие задачи также являются NP-трудными . [примечание 2] Это делается путем полиномиального сокращения времени от 3-SAT до другой проблемы. Примером задачи, в которой использовался этот метод, является задача о клике : для формулы CNF, состоящей из c предложений, соответствующий граф состоит из вершины для каждого литерала и ребра между каждыми двумя непротиворечивыми [примечание 3] литералами . из разных статей, см. картина. Граф имеет c -клику тогда и только тогда, когда формула выполнима. [11]
Существует простой рандомизированный алгоритм, предложенный Шёнингом (1999), который работает за время (4/3) n , где n — количество переменных в предложении 3-SAT, и позволяет с высокой вероятностью правильно решить 3-SAT. [12]
Гипотеза экспоненциального времени утверждает, что ни один алгоритм не может решить 3-SAT (или даже k -SAT для любого ) за время exp( o ( n )) (т. е. существенно быстрее, чем экспоненциальное за n ).
Селман, Митчелл и Левеск (1996) приводят эмпирические данные о сложности случайно сгенерированных формул 3-SAT в зависимости от их параметров размера. Сложность измеряется количеством рекурсивных вызовов, выполняемых алгоритмом DPLL . Они определили область фазового перехода от почти наверняка выполнимых к почти наверняка невыполнимым формулам при соотношении предложений к переменным около 4,26. [13]
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 может быть дополнено фиксированными фиктивными переменными до l 1 ∨ ⋯ ∨ l j ∨ d j + 1 ∨ ⋯ ∨ d k . После заполнения всех предложений необходимо добавить 2 k -1 дополнительных предложений [примечание 4] , чтобы гарантировать, что только d 1 = ⋯ = d k =FALSE может привести к удовлетворительному присваиванию. Поскольку k не зависит от длины формулы, дополнительные предложения приводят к постоянному увеличению длины. По той же причине не имеет значения, разрешены ли в предложениях повторяющиеся литералы , как в ¬ x ∨ ¬ y ∨ ¬ y .
Конъюнктивная нормальная форма (в частности, с тремя литералами в предложении) часто считается каноническим представлением формул SAT. Как показано выше, общая проблема SAT сводится к 3-SAT, задаче определения выполнимости формул в этой форме.
SAT тривиален, если формулы ограничены формулами в дизъюнктивной нормальной форме , то есть они представляют собой дизъюнкцию конъюнкций литералов. Такая формула действительно выполнима тогда и только тогда, когда хотя бы одна из ее конъюнкций выполнима, а конъюнкция выполнима тогда и только тогда, когда она не содержит одновременно x и NOT x для некоторой переменной x . Это можно проверить за линейное время. Более того, если они ограничены полной дизъюнктивной нормальной формой , в которой каждая переменная появляется ровно один раз в каждой конъюнкции, их можно проверить за постоянное время (каждая конъюнктура представляет одно удовлетворяющее присваивание). Но для преобразования общей задачи SAT в дизъюнктивную нормальную форму может потребоваться экспоненциальное время и пространство; для примера поменяйте местами «∧» и «∨» в приведенном выше примере экспоненциального разрушения для конъюнктивных нормальных форм.
Вариантом проблемы выполнимости 3 является 3-SAT «один из трех» (также известный как «1 из 3-SAT» и «точно 1 3-SAT» ). Учитывая конъюнктивную нормальную форму с тремя литералами в каждом предложении, проблема состоит в том, чтобы определить, существует ли истинное присвоение переменным так, чтобы каждое предложение имело ровно один TRUE литерал (и, следовательно, ровно два FALSE литерала). Напротив, обычный 3-SAT требует, чтобы каждое предложение имело хотя бы один TRUE-литерал. Формально задача 3-SAT «один из трех» задается как обобщенная конъюнктивная нормальная форма со всеми обобщенными предложениями, использующими тернарный оператор R , который имеет значение ИСТИНА только в том случае, если только один из его аргументов является истинным. Когда все литералы формулы 3-SAT «один к трем» положительны, проблема выполнимости называется положительной 3-SAT «один к трем» .
Один из трех 3-SAT вместе с его положительным случаем указан как NP-полная проблема «LO4» в стандартном справочнике Майкла Р. Гари и Дэвида «Компьютеры и трудноразрешимость: руководство по теории NP-полноты» . С. Джонсон . Томас Джером Шефер доказал, что 3-SAT «один из трех» является NP-полным как частный случай теоремы о дихотомии Шефера , которая утверждает, что любая проблема, обобщающая булеву выполнимость определенным образом, находится либо в классе P, либо является NP- полный. [14]
Шефер предлагает конструкцию, позволяющую легко за полиномиальное время сократить 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 равен TRUE, см. рисунок (слева). Таким образом, любой экземпляр 3-SAT с m предложений и n переменными может быть преобразован в эквивалентный экземпляр 3-SAT «один из трех» с 5 m предложений и n +6 m переменных. [15] Другая редукция включает только четыре новые переменные и три предложения: R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R( c , d , ¬ z ), см. рисунок (справа).
Другой вариант — проблема не-всего равного 3-выполнимости (также называемая NAE3SAT ). Учитывая конъюнктивную нормальную форму с тремя литералами в каждом предложении, проблема состоит в том, чтобы определить, существует ли присвоение переменным такое, что ни в одном предложении все три литерала не имеют одинаковое значение истинности. Эта проблема также является NP-полной, даже если в соответствии с теоремой Шефера о дихотомии не допускаются символы отрицания. [14]
Формула 3-SAT называется линейной SAT ( LSAT ), если каждое предложение (рассматриваемое как набор литералов) пересекает не более одного другого предложения, и, более того, если два предложения пересекаются, то они имеют ровно один общий литерал. Формулу LSAT можно изобразить как набор непересекающихся полузамкнутых интервалов на линии. Решение о выполнимости формулы LSAT является NP-полным. [16]
SAT проще, если количество литералов в предложении ограничено максимум двумя, и в этом случае проблема называется 2-SAT . Эта задача может быть решена за полиномиальное время и фактически является полной для класса сложности NL . Если дополнительно все операции ИЛИ в литералах заменяются операциями XOR , результат называется исключающей или 2-выполнимостью , что является полной задачей для класса сложности SL = L.
Проблема определения выполнимости данного соединения предложений Хорна называется Хорн-выполнимостью , или HORN-SAT . Ее можно решить за полиномиальное время с помощью одного шага алгоритма распространения единиц , который создает единственную минимальную модель набора предложений Хорна (относительно набора литералов, которым присвоено значение TRUE). Хорн-выполнимость P-полна . Ее можно рассматривать как версию проблемы булевой выполнимости, предложенную P. Кроме того, определение истинности количественных формул Хорна может быть выполнено за полиномиальное время. [17]
Предложения Хорна представляют интерес, поскольку они способны выражать импликацию одной переменной из набора других переменных. Действительно, одно такое предложение ¬ x 1 ∨ ... ∨ ¬ x n ∨ y можно переписать как x 1 ∧ ... ∧ x n → y , то есть, если все x 1 ,..., x n ИСТИННЫ. , то y также должно быть TRUE.
Обобщением класса формул Хорна являются формулы переименовываемого Хорна, которые представляют собой набор формул, которые можно поместить в форму Хорна путем замены некоторых переменных их соответствующим отрицанием. Например, ( 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, поскольку ее можно решить, сначала выполнив эту замену, а затем проверив выполнимость полученной формулы Хорна.
Другим особым случаем является класс задач, где каждое предложение содержит операторы XOR (т. е. исключающее или ), а не (простые) операторы OR. [примечание 5] Это в P , поскольку формулу XOR-SAT также можно рассматривать как систему линейных уравнений по модулю 2 и можно решать за кубическое время методом исключения Гаусса ; [18] см. пример в рамке. Эта переработка основана на родстве между булевыми алгебрами и булевыми кольцами , а также на том факте, что арифметика по модулю два образует конечное поле . Поскольку XOR b XOR c оценивается как TRUE тогда и только тогда, когда ровно 1 или 3 члена { a , b , c } имеют значение TRUE , каждое решение задачи 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 является частным случаем этой теоремы. [14]
В следующей таблице приведены некоторые распространенные варианты SAT.
Расширение, получившее значительную популярность с 2003 года, — это теории выполнимости по модулю ( SMT ), которые могут обогащать формулы CNF линейными ограничениями, массивами, совершенно разными ограничениями, неинтерпретируемыми функциями , [19] и т. д . Такие расширения обычно остаются NP-полными, но очень Теперь доступны эффективные решатели, которые могут обрабатывать многие виды ограничений.
Проблема выполнимости становится более сложной, если кванторам «для всех» ( ∀ ) и «существует» ( ∃ ) разрешено связывать логические переменные. Примером такого выражения может быть ∀ x ∀ y ∃ z ( x ∨ y ∨ z ) ∧ (¬ x ∨ ¬ y ∨ ¬ z ) ; это действительно так, поскольку для всех значений x и y можно найти подходящее значение z , а именно. z = ИСТИНА, если и x , и y имеют значение ЛОЖЬ, и z = ЛОЖЬ в противном случае. Сам SAT (молчаливо) использует только ∃-кванторы. Если вместо этого разрешены только кванторы ∀, получается так называемая проблема тавтологии , которая является ко-NP-полной . Если разрешены оба квантора, проблема называется проблемой количественной булевой формулы ( QBF ), которая, как можно показать, является PSPACE-полной . Широко распространено мнение, что задачи, полные по PSPACE, строго сложнее, чем любая задача в NP, хотя это еще не доказано. Используя высокопараллельные P-системы , проблемы QBF-SAT можно решать за линейное время. [20]
Обычный SAT спрашивает, есть ли хотя бы одно присвоение переменной, которое делает формулу истинной. Разнообразие вариантов касается количества таких заданий:
Другие обобщения включают выполнимость для логики первого и второго порядка , задачи удовлетворения ограничений , целочисленное программирование 0-1 .
В то время как SAT является проблемой решения , проблема поиска удовлетворяющего задания сводится к SAT. То есть каждый алгоритм, который правильно отвечает, разрешима ли задача SAT, может быть использован для поиска удовлетворяющего задания. Сначала задается вопрос по данной формуле Φ. Если ответ «нет», формула невыполнима. В противном случае вопрос задается по частично конкретизированной формуле Φ { x 1 =TRUE} , т.е. Φ с первой переменной x 1 , замененной на TRUE и упрощенной соответственно. Если ответ «да», то x 1 =ИСТИНА, в противном случае x 1 =ЛОЖЬ. Значения остальных переменных можно найти впоследствии таким же образом. Всего требуется n +1 запуск алгоритма, где n — количество различных переменных в Φ.
Это свойство используется в нескольких теоремах теории сложности:
Поскольку задача SAT является NP-полной, для нее известны только алгоритмы с экспоненциальной сложностью в худшем случае. Несмотря на это, эффективные и масштабируемые алгоритмы для SAT были разработаны в 2000-х годах и способствовали значительному прогрессу в нашей способности автоматически решать примеры задач, включающие десятки тысяч переменных и миллионы ограничений (т.е. предложений). [1] Примеры таких проблем в автоматизации электронного проектирования (EDA) включают формальную проверку эквивалентности , проверку модели , формальную проверку конвейерных микропроцессоров , [19] автоматическую генерацию тестовых шаблонов , маршрутизацию FPGA , [26] планирование и задачи планирования , и скоро. Механизм решения SAT также считается важным компонентом в наборе инструментов автоматизации проектирования электроники .
Основные методы, используемые современными решателями SAT, включают алгоритм Дэвиса-Патнэма-Логеманна-Лавленда (или DPLL), обучение предложений, управляемое конфликтами (CDCL), и алгоритмы стохастического локального поиска, такие как WalkSAT . Почти все решатели SAT имеют тайм-ауты, поэтому они завершатся в разумные сроки, даже если не смогут найти решение. Разные решатели SAT найдут разные случаи легкими или трудными, и некоторые преуспевают в доказательстве невыполнимости, а другие в поиске решений. Недавние попытки были предприняты для изучения выполнимости экземпляра с использованием методов глубокого обучения. [27]
Решатели SAT разрабатываются и сравниваются в конкурсах по решению SAT. [28] Современные решатели SAT также оказывают значительное влияние на области верификации программного обеспечения, решения ограничений в искусственном интеллекте и исследования операций, среди прочего.
современные решатели SAT часто могут решать задачи с миллионами ограничений и сотнями тысяч переменных..
(по дате публикации)