stringtranslate.com

Проблема выполнимости булевых уравнений

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

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

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

Определения

Формула пропозициональной логики , также называемая булевым выражением , строится из переменных , операторов AND ( конъюнкция , также обозначается как ∧), OR ( дизъюнкция , ∨), NOT ( отрицание , ¬) и скобок. Формула считается выполнимой, если ее можно сделать ИСТИННОЙ, присвоив ее переменным соответствующие логические значения (т. е. ИСТИНА, ЛОЖЬ). Задача выполнимости булевой формулы (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  = ЛОЖЬ, x 2  = ЛОЖЬ и x 3 произвольно, так как (ЛОЖЬ ∨ ¬ЛОЖЬ) ∧ (¬ЛОЖЬ ∨ ЛОЖЬ ∨ x 3 ) ∧ ¬ЛОЖЬ оценивается как (ЛОЖЬ ∨ ИСТИНА) ∧ (ИСТИНА ∨ ЛОЖЬ ∨ x 3 ) ∧ ИСТИНА, и в свою очередь как ИСТИНА ∧ ИСТИНА ∧ ИСТИНА (т. е. ИСТИНА). Напротив, формула CNF a ∧ ¬ a , состоящая из двух предложений одного литерала, невыполнима, так как для a = ИСТИНА или a = ЛОЖЬ она оценивается как ИСТИНА ∧ ¬ИСТИНА (т. е. ЛОЖЬ) или ЛОЖЬ ∧ ¬ЛОЖЬ (т. е. снова ЛОЖЬ) соответственно.

Для некоторых версий задачи 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 ) в конъюнктивную нормальную форму дает

( х 1  ∨  х 2  ∨ … ∨  х n ) ∧
( y 1  ∨  Икс 2  ∨ … ∨  Икс п ) ∧
( Икс 1  ∨  y 2  ∨ … ∨  Икс п ) ∧
( y 1  ∨  y 2  ∨ … ∨  Икс п ) ∧ ... ∧
( Икс 1  ∨  Икс 2  ∨ … ∨  y п ) ∧
( y 1  ∨  Икс 2  ∨ … ∨  y п ) ∧
( Икс 1  ∨  y 2  ∨ … ∨  y п ) ∧
( у 1  ∨  у 2  ∨ … ∨  у n ) ;

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

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

Сложность

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

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

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

Экземпляр 3-SAT ( x ∨ x ∨ y ) ∧ (¬ x ∨ ¬ y ∨ ¬ y ) ∧ (¬ x ∨ y ∨ y ) сводится к проблеме клики . Зеленые вершины образуют 3-клику и соответствуют удовлетворяющему назначению x = ЛОЖЬ, y = ИСТИНА.

Как и проблема выполнимости для произвольных формул, определение выполнимости формулы в конъюнктивной нормальной форме, где каждое предложение ограничено максимум тремя литералами, также является NP-полной задачей; эта задача называется 3-SAT , 3CNFSAT или 3-выполнимостью . Чтобы свести неограниченную задачу SAT к 3-SAT, преобразуем каждое предложение l 1 ∨ ⋯ ∨ l n в конъюнкцию n - 2 предложений

( л 1 ∨ л 2 ∨ х 2 ) ∧
(¬ х 2 ∨ л 3 ∨ х 3 ) ∧
(¬ х 3 ∨ л 4 ∨ х 4 ) ∧ ⋯ ∧
(¬ x n −3 ∨ l n −2 ∨ x n −2 ) ∧
(¬ x n −2 ∨ l n −1 ∨ l n )

где 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 для любого k > 2 ) за время 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

Конъюнктивная нормальная форма

Конъюнктивная нормальная форма (в частности, с 3 литералами на предложение) часто считается каноническим представлением для формул SAT. Как показано выше, общая проблема SAT сводится к 3-SAT, проблеме определения выполнимости формул в этой форме.

Дизъюнктивная нормальная форма

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

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

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

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

One-in-three 3-SAT, вместе с его положительным случаем, указана как NP-полная задача "LO4" в стандартном справочнике Computers and Intractability: A Guide to the Theory of NP-Completeness Майкла Р. Гэри и Дэвида С. Джонсона . Было доказано, что One-in-three 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 является ИСТИНА, см. рисунок (слева). Таким образом, любой экземпляр 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-выполнимость

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

Линейный SAT

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

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

SAT проще, если количество литералов в предложении ограничено максимум 2, в этом случае задача называется 2-SAT . Эта задача может быть решена за полиномиальное время и фактически является полной для класса сложности NL . Если дополнительно все операции OR в литералах заменить на операции 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 также должен быть ИСТИННЫМ.

Обобщением класса формул Хорна является класс переименовываемых формул Хорна, представляющих собой набор формул, которые можно представить в форме Хорна, заменив некоторые переменные их соответствующим отрицанием. Например, ( 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-выполнимость

Другим особым случаем является класс задач, где каждое предложение содержит XOR (т. е. исключающее ИЛИ ), а не (простые) операторы ИЛИ. [примечание 5] Это в P , поскольку формулу XOR-SAT можно также рассматривать как систему линейных уравнений mod 2 и можно решить за кубическое время методом исключения Гаусса ; [18] см. пример во вставке. Эта переработка основана на родстве между булевыми алгебрами и булевыми кольцами , а также на том факте, что арифметика по модулю два образует конечное поле . Поскольку XOR b XOR c оценивается как ИСТИНА, если и только если ровно 1 или 3 члена { a , b , c } являются ИСТИННЫМИ, каждое решение задачи 1-in-3-SAT для данной формулы CNF также является решением задачи XOR-3-SAT, и, в свою очередь, каждое решение XOR-3-SAT является решением 3-SAT; см. рисунок. Вследствие этого для каждой формулы CNF можно решить задачу XOR-3-SAT, определяемую этой формулой, и на основании результата сделать вывод о том, что задача 3-SAT разрешима или что задача 1-in-3-SAT неразрешима.

При условии, что классы сложности P и NP не равны , ни 2-, ни Хорн-, ни XOR-выполнимость не являются NP-полными, в отличие от SAT.

Теорема Шефера о дихотомии

Приведенные выше ограничения (CNF, 2CNF, 3CNF, Horn, XOR-SAT) связывают рассматриваемые формулы с конъюнкциями подформул; каждое ограничение устанавливает определенную форму для всех подформул: например, только бинарные предложения могут быть подформулами в 2CNF.

Теорема Шефера о дихотомии утверждает, что для любого ограничения на булевы функции, которые могут быть использованы для формирования этих подформул, соответствующая проблема выполнимости находится в P или NP-полной. Принадлежность к P выполнимости формул 2CNF, Horn и XOR-SAT является частным случаем этой теоремы. [14]

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

Расширения SAT

Расширение, которое приобрело значительную популярность с 2003 года, — это теории выполнимости по модулю ( SMT ), которые могут обогатить формулы CNF линейными ограничениями, массивами, всеразличными ограничениями, неинтерпретируемыми функциями [19] и т. д. Такие расширения обычно остаются NP-полными, но теперь доступны очень эффективные решатели, которые могут обрабатывать многие виды таких ограничений.

Проблема выполнимости становится более сложной, если кванторы «для всех» ( ∀ ) и «существует» ( ∃ ) разрешены для связывания булевых переменных. Примером такого выражения может быть ∀ x ∀ y ∃ z ( x ∨ y ∨ z ) ∧ (¬ x ∨ ¬ y ∨ ¬ z ) ; оно допустимо, поскольку для всех значений x и y может быть найдено соответствующее значение z , а именно z =TRUE, если и x, и y являются FALSE, и z =FALSE в противном случае. Сам SAT (неявно) использует только кванторы ∃. Если вместо этого разрешены только кванторы ∀ , получается так называемая проблема тавтологии , которая является co-NP-полной . Если оба квантификатора разрешены, то проблема называется квантифицированной проблемой булевой формулы ( QBF ), которая, как можно показать, является PSPACE-полной . Широко распространено мнение, что PSPACE-полные проблемы строго сложнее, чем любые проблемы в NP, хотя это еще не доказано. Используя высокопараллельные системы P , проблемы QBF-SAT могут быть решены за линейное время. [20]

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

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

Поиск удовлетворяющего задания

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

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

NP ⊆ P/poly ⇒ PH = Σ 2   ( теорема Карпа–Липтона )
НП ⊆ БПП ⇒ НП = РП
П = НП ⇒ ФП = ФНП

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

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

Основные методы, используемые современными решателями SAT, включают алгоритм Дэвиса–Патнэма–Логеманна–Лавленда (или DPLL), обучение на основе конфликтных положений (CDCL) и алгоритмы стохастического локального поиска , такие как WalkSAT . Почти все решатели SAT включают тайм-ауты, поэтому они завершат работу в разумные сроки, даже если не смогут найти решение. Различные решатели SAT найдут разные примеры легкими или сложными, и некоторые преуспеют в доказательстве невыполнимости, а другие в поиске решений. Недавно [ когда? ] были предприняты попытки изучить выполнимость примера с использованием методов глубокого обучения. [27]

Решатели SAT разрабатываются и сравниваются в соревнованиях по решению SAT. [28] Современные решатели SAT также оказывают значительное влияние на области верификации программного обеспечения, решения ограничений в искусственном интеллекте и исследования операций, среди прочих.

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

Примечания

  1. ^ Задача SAT для произвольных формул также является NP-полной, поскольку легко показать, что она принадлежит NP, и она не может быть проще, чем SAT для формул CNF.
  2. ^ т.е. по крайней мере такая же сложная, как и любая другая задача из NP. Задача принятия решения является NP-полной тогда и только тогда, когда она находится в NP и является NP-трудной.
  3. ^ т.е. такой, что один литерал не является отрицанием другого
  4. ^ а именно все макстермы , которые могут быть построены с d 1 ,⋯, d k , за исключением d 1 ∨⋯∨ d k
  5. ^ Формально используются обобщенные конъюнктивные нормальные формы с тернарной булевой функцией R , которая ИСТИНА только тогда, когда 1 или 3 ее аргумента ИСТИНА. Входное предложение с более чем 3 литералами может быть преобразовано в равновыполнимую конъюнкцию предложений по 3 литерала, аналогичную приведенной выше; т. е. XOR-SAT может быть сведена к XOR-3-SAT.

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

На Викискладе есть медиафайлы по теме «Проблема выполнимости булевых уравнений» .

Ссылки

  1. ^ ab Ohrimenko, Olga; Stuckey, Peter J.; Codish, Michael (2007), "Распространение = ленивая генерация предложений", Principles and Practice of Constraint Programming – CP 2007 , Lecture Notes in Computer Science, т. 4741, стр. 544–558, CiteSeerX  10.1.1.70.5471 , doi :10.1007/978-3-540-74970-7_39, ISBN 978-3-540-74969-1Современные решатели SAT часто могут решать задачи с миллионами ограничений и сотнями тысяч переменных..
  2. ^ Хонг, Тед; Ли, Яньцзин; Парк, Сунг-Бом; Муи, Диана; Лин, Дэвид; Калек, Зияд Абдель; Хаким, Нагиб; Наими, Хелия; Гарднер, Дональд С.; Митра, Субхасиш (ноябрь 2010 г.). "QED: Тесты быстрого обнаружения ошибок для эффективной проверки после кремния". Международная конференция по тестированию IEEE 2010 г. стр. 1–10. doi :10.1109/TEST.2010.5699215. ISBN 978-1-4244-7206-2. S2CID  7909084.
  3. ^ Карп, Ричард М. (1972). «Сводимость среди комбинаторных задач» (PDF) . В Raymond E. Miller; James W. Thatcher (ред.). Сложность компьютерных вычислений . Нью-Йорк: Plenum. стр. 85–103. ISBN 0-306-30707-3. Архивировано из оригинала (PDF) 2011-06-29 . Получено 2020-05-07 .Здесь: стр.86
  4. ^ Ахо, Альфред В.; Хопкрофт, Джон Э.; Ульман, Джеффри Д. (1974). Проектирование и анализ компьютерных алгоритмов . Addison-Wesley. стр. 403. ISBN 0-201-00029-6.
  5. ^ Массаччи, Фабио; Марраро, Лаура (2000-02-01). «Логический криптоанализ как проблема SAT». Журнал автоматизированного рассуждения . 24 (1): 165–203. doi :10.1023/A:1006326723002. S2CID  3114247.
  6. ^ Миронов, Илья; Чжан, Линтао (2006). «Применение SAT Solvers для криптоанализа хэш-функций». В Biere, Armin; Gomes, Carla P. (ред.). Теория и применение тестирования выполнимости — SAT 2006. Конспект лекций по информатике. Том 4121. Springer. С. 102–115. doi :10.1007/11814948_13. ISBN 978-3-540-37207-3.
  7. ^ Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). «Решатели булевой выполнимости и их применение в проверке моделей». Труды IEEE . 103 (11): 2021–2035. doi :10.1109/JPROC.2015.2455034. S2CID  10190144.
  8. ^ Кук, Стивен А. (1971). "Сложность процедур доказательства теорем" (PDF) . Труды третьего ежегодного симпозиума ACM по теории вычислений - STOC '71 . стр. 151–158. CiteSeerX 10.1.1.406.395 . doi :10.1145/800157.805047. S2CID  7573663. Архивировано (PDF) из оригинала 2022-10-09. 
  9. ^ Левин, Леонид (1973). «Универсальные задачи поиска». Проблемы передачи информации . 9 (3): 115–116.(pdf) (на русском языке) , переведено на английский Трахтенбротом, BA (1984). "Обзор российских подходов к алгоритмам перебора (перебора)". Annals of the History of Computing . 6 (4): 384–400. doi :10.1109/MAHC.1984.10036. S2CID  950581.
  10. ^ Ахо, Хопкрофт и Ульман (1974), Теорема 10.4.
  11. ^ Ахо, Хопкрофт и Ульман (1974), Теорема 10.5.
  12. ^ Шёнинг, Уве (октябрь 1999 г.). «Вероятностный алгоритм для k-SAT и проблем удовлетворения ограничений» (PDF) . 40-й ежегодный симпозиум по основам компьютерной науки (Кат. № 99CB37039) . стр. 410–414. doi :10.1109/SFFCS.1999.814612. ISBN 0-7695-0409-4. S2CID  123177576. Архивировано (PDF) из оригинала 09.10.2022.
  13. ^ Селман, Барт; Митчелл, Дэвид; Левек, Гектор (1996). «Создание проблем с трудной выполнимостью». Искусственный интеллект . 81 (1–2): 17–29. CiteSeerX 10.1.1.37.7362 . doi :10.1016/0004-3702(95)00045-3. 
  14. ^ abc Шефер, Томас Дж. (1978). "Сложность проблем выполнимости" (PDF) . Труды 10-го ежегодного симпозиума ACM по теории вычислений . Сан-Диего, Калифорния. С. 216–226. CiteSeerX 10.1.1.393.8951 . doi :10.1145/800133.804350. 
  15. ^ Шефер (1978), стр. 222, Лемма 3.5.
  16. ^ Аркин, Эстер М.; Баник, Аритра; Карми, Пас; Цитовский, Гуи; Кац, Мэтью Дж.; Митчелл, Джозеф СБ; Симаков, Марина (2018-12-11). «Выбор и покрытие цветных точек». Дискретная прикладная математика . 250 : 75–86. doi : 10.1016/j.dam.2018.05.011 . ISSN  0166-218X.
  17. ^ Buning, HK; Karpinski, Marek; Flogel, A. (1995). «Разрешение для квантифицированных булевых формул». Информация и вычисления . 117 (1). Elsevier: 12–18. doi : 10.1006/inco.1995.1025 .
  18. ^ Мур, Кристофер ; Мертенс, Стефан (2011), Природа вычислений, Oxford University Press, стр. 366, ISBN 9780199233212.
  19. ^ ab RE Bryant, SM German и MN Velev, Микропроцессорная верификация с использованием эффективных процедур принятия решений для логики равенства с неинтерпретируемыми функциями, в Analytic Tableaux and Related Methods, стр. 1–13, 1999.
  20. ^ Алхазов, Артём; Мартин-Виде, Карлос; Пан, Линьцян (2003). «Решение полной задачи PSPACE путем распознавания P-систем с ограниченными активными мембранами». Fundamenta Informaticae . 58 : 67–77.Здесь: Раздел 3, Тема 3.1
  21. ^ Бласс, Андреас; Гуревич, Юрий (1 октября 1982 г.). «О проблеме уникальной выполнимости». Информация и управление . 55 (1): 80–88. doi : 10.1016/S0019-9958(82)90439-9 . hdl : 2027.42/23842 . ISSN  0019-9958.
  22. ^ "Complexity Zoo:U - Complexity Zoo". difficultyzoo.uwaterloo.ca . Архивировано из оригинала 2019-07-09 . Получено 2019-12-05 .
  23. ^ Козен, Декстер К. (2006). "Дополнительная лекция F: Уникальная выполнимость". Теория вычислений . Тексты по информатике. Springer. стр. 180. ISBN 9781846282973.
  24. ^ Валиант, Л.; Вазирани, В. (1986). «NP так же просто, как обнаружение уникальных решений» (PDF) . Теоретическая информатика . 47 : 85–93. doi : 10.1016/0304-3975(86)90135-0 .
  25. ^ Булдас, Ахто; Ленин, Александр; Виллемсон, Ян; Чарнаморд, Антон (2017). «Простые сертификаты невыполнимости для деревьев атак». В Обана, Сатоши; Чида, Кодзи (ред.). Достижения в области информационной и компьютерной безопасности . Конспект лекций по информатике. Том 10418. Springer International Publishing. стр. 39–55. doi :10.1007/978-3-319-64200-0_3. ISBN 9783319642000.
  26. ^ Gi-Joon Nam; Sakallah, KA; Rutenbar, RA (2002). "Новый подход к подробной маршрутизации ПЛИС с помощью поисковой логической выполнимости" (PDF) . IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems . 21 (6): 674. doi :10.1109/TCAD.2002.1004311. Архивировано из оригинала (PDF) 2016-03-15 . Получено 2015-09-04 .
  27. ^ Selsam, Daniel; Lamm, Matthew; Bünz, Benedikt; Liang, Percy; de Moura, Leonardo; Dill, David L. (11 марта 2019 г.). «Изучение решателя SAT с помощью однобитового надзора». arXiv : 1802.03685 [cs.AI].
  28. ^ "Веб-страница международных соревнований SAT" . Получено 2007-11-15 .

Источники

Дальнейшее чтение

(по дате публикации)