Введение

Проблема определения, может ли булева формула быть истинной.

В логике и информатике проблема булевой выполнимости (иногда называемая проблемой выполнимости пропозициональных формул и сокращенно SATISFIABILITY, SAT или B SAT) — это задача определения, существует ли интерпретация, удовлетворяющая заданной булевой формуле. Иными словами, она спрашивает, можно ли последовательно заменить переменные заданной булевой формулы значениями ИСТИНА или ЛОЖЬ таким образом, чтобы формула вычислялась как ИСТИНА. Если это так, формула называется выполнимой. С другой стороны, если такого присваивания не существует, функция, выраженная формулой, является ЛОЖЬ для всех возможных присваиваний переменных, и формула является невыполнимой. Например, формула "a И НЕ b" выполнима, поскольку можно найти значения a = ИСТИНА и b = ЛОЖЬ, при которых (a И НЕ b) = ИСТИНА. В отличие от этого, "a И НЕ a" является невыполнимой. SAT — первая задача, доказанная NP-полной; см. теорему Кука — Левина. Это означает, что все задачи класса сложности NP, включающие широкий спектр естественных задач принятия решений и оптимизации, по крайней мере, столь же сложны для решения, как и задача SAT. Не существует известного алгоритма, эффективно решающего каждую задачу SAT, и обычно считается, что такого алгоритма не существует; однако это убеждение не было математически доказано, и решение вопроса о том, существует ли у SAT алгоритм полиномиального времени, эквивалентно проблеме P против NP, которая является известной открытой проблемой в теории вычислений. Тем не менее, по состоянию на 2007 год эвристические алгоритмы SAT способны решать экземпляры задач, включающие десятки тысяч переменных и формулы, состоящие из миллионов символов, а также автоматическое доказательство теорем.

Определения

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

Сложность

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

Соединительная нормальная форма

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

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

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

Не все одинаково 3-удовлетворительность

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

2-удовлетворительность

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

Удовлетворительность рога

Проблема определения выполнимости данного союза клауз Хорна называется выполнимостью Хорна, или HORN SAT. Её можно решить за полиномиальное время одним шагом алгоритма распространения единиц, который генерирует единственную минимальную модель набора клауз Хорна (относительно набора литералов, присвоенных значению ИСТИНА). Выполнимость Хорна является P-полной. Её можно рассматривать как версию задачи о выполнимости булевых формул для класса P. Кроме того, определение истинности квантифицированных формул Хорна также может быть выполнено за полиномиальное время. Клаузы Хорна представляют интерес, поскольку они позволяют выразить следование одной переменной из набора других переменных. Действительно, такая клауза ¬x1 ∨ … ∨ ¬xn ∨ y может быть переписана как x1 ∧ … ∧ xn → y, то есть, если x1, …, xn все ИСТИННЫ, то y также должна быть ИСТИННОЙ. Обобщением класса формул Хорна является класс переименовываемых формул Хорна, представляющий собой набор формул, которые можно привести к форме Хорна, заменив некоторые переменные на их отрицания. Например, (x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1 не является формулой Хорна, но может быть переименована в формулу Хорна (x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ ¬y3) ∧ ¬x1 путем введения y3 как отрицания x3. В отличие от этого, никакое переименование (x1 ∨ ¬x2 ∨ ¬x3) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1 не приводит к формуле Хорна. Проверка существования такой замены может быть выполнена за линейное время; следовательно, выполнимость таких формул находится в классе P, поскольку её можно решить, сначала выполнив эту замену, а затем проверив выполнимость полученной формулы Хорна.

Удовлетворительность XOR

Решение примера XOR SAT методом гауссова исключения. Для данной формулы ("⊕" означает XOR, the необязательно): (a⊕c⊕d) ∧ (b⊕¬c⊕d) ∧ (a⊕b⊕¬d) ∧ (a⊕¬b⊕¬c). Система уравнений ("1" означает TRUE, "0" означает FALSE). Каждое слагаемое приводит к одному уравнению: a ⊕ c ⊕ d = 1, b ⊕ ¬c ⊕ d = 1, a ⊕ b ⊕ ¬d = 1, a ⊕ ¬b ⊕ ¬c = 1. Нормализованная система уравнений, использующая свойства булевых колец (¬x = 1 ⊕ x, x ⊕ x = 0): a ⊕ c ⊕ d = 1, b ⊕ c ⊕ d = 0, a ⊕ b ⊕ d = 0, a ⊕ b ⊕ c = 1. (Если "⊕" присутствует, это противоречит последнему черному уравнению, поэтому система неразрешима. Следовательно, алгоритм Гаусса используется только для черных уравнений.) Связанная матрица коэффициентов:
a b c d
1 0 1 1
0 1 1 1
1 1 0 1
1 1 1 0
Преобразование к ступенчатому виду:
a b c d Операция
1 0 1 1 A
0 1 1 1 B
1 1 0 1 C
1 1 1 0 D
1 0 1 1 A
1 1 0 1 C
1 1 1 0 D
0 1 1 1 B (поменяли местами)
1 0 1 1 A
0 1 1 0 1 E = C⊕A
0 1 0 1 0 F = D⊕A
0 1 1 1 0 B
1 0 1 1 A
0 1 1 0 1 E
0 0 1 1 1 G = F⊕E
0 0 0 1 1 H = B⊕E
Преобразование к диагональному виду:
a b c d Операция
1 0 1 0 0 I = A⊕H
0 1 1 0 1 E
0 0 1 0 0 J = G⊕H
0 0 0 1 1 H
1 0 0 0 0 K = I⊕J
0 1 0 0 1 L = E⊕J
0 0 1 0 0 J
0 0 0 1 1 H
Решение: Если "⊕" присутствует: Неразрешимо. Иначе: a = 0 = FALSE, b = 1 = TRUE, c = 0 = FALSE, d = 1 = TRUE. Как следствие: (a⊕c⊕d) ∧ (b⊕¬c⊕d) ∧ (a⊕b⊕¬d) ∧ (a⊕¬b⊕¬c) не выполняется в 3 удовлетворяющих случаях, в то время как (a ∨ c ∨ d) ∧ (b ∨ ¬c ∨ d) ∧ (a ∨ b ∨ ¬d) ∧ (a ∨ ¬b ∨ ¬c) выполняется в 3 удовлетворяющих случаях при a=c=FALSE и b=d=TRUE. Другой особый случай – это класс задач, где каждое слагаемое содержит XOR (т.е. исключающее ИЛИ), а не (простое) OR. Эта задача относится к классу P, поскольку формулу XOR SAT также можно рассматривать как систему линейных уравнений по модулю 2, которую можно решить за кубическое время методом гауссова исключения; см. пример в рамке. Это преобразование основано на связи между булевыми алгебрами и булевыми кольцами, а также на том факте, что арифметика по модулю два образует конечное поле. Поскольку a 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-SAT, ни Horn-SAT, ни XOR-удовлетворимость не являются NP-полными, в отличие от SAT.

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

Вышеуказанные ограничения (CNF, 2CNF, 3CNF, Horn, XOR SAT) ограничивают рассматриваемые формулы как союзы подформул; каждое ограничение определяет конкретную форму для всех подформул: например, в 2CNF подформулами могут быть только двоичные клаузы. Теорема о дихотомии Шефера утверждает, что для любого ограничения булевых функций, используемых для формирования этих подформул, соответствующая задача выполнимости либо находится в классе P, либо является NP-полной. Принадлежность задач выполнимости для формул 2CNF, Horn и XOR SAT является частными случаями этой теоремы. и т.д. Такие расширения обычно остаются NP-полными, но в настоящее время доступны высокоэффективные решатели, способные обрабатывать многие подобные виды ограничений. Задача выполнимости становится сложнее, если разрешено использовать кванторы всеобщности (∀) и существования (∃) для связывания булевых переменных. Примером такого выражения является size=100%; оно выполнимо, поскольку для всех значений x и y можно найти соответствующее значение z, а именно: z=TRUE, если и x, и y ложны, и z=FALSE в противном случае. Сам SAT (по умолчанию) использует только квантор существования (∃). Если вместо этого разрешены только кванторы всеобщности (∀), получается так называемая задача проверки тавтологии, которая является co NP-полной. Если разрешены оба квантора, задача называется задачей квантованной булевой формулы (QBF), которая может быть показана PSPACE-полной. Широко распространено мнение, что PSPACE-полные задачи строго сложнее любых задач в NP, хотя это пока не доказано. С использованием высокопараллельных P-систем задачи QBF SAT могут быть решены за линейное время. Обычная задача SAT спрашивает, существует ли хотя бы одно присваивание переменных, делающее формулу истинной. Различные варианты рассматривают количество таких присваиваний: MAJ SAT спрашивает, делает ли большинство всех присваиваний формулу истинной. Известно, что она является полной для PP, вероятностного класса. #SAT, задача подсчета количества присваиваний переменных, удовлетворяющих формуле, является задачей подсчета, а не задачей принятия решения, и является #P-полной. UNIQUE SAT – это задача определения, имеет ли формула ровно одно присваивание, удовлетворяющее ей. Она является полной для US, класса сложности, описывающего задачи, разрешимые недетерминированной машиной Тьюринга за полиномиальное время, которая принимает, когда существует ровно один недетерминированный путь принятия, и отклоняет в противном случае. UNAMBIGUOUS SAT – это название задачи выполнимости, когда вход ограничен формулами, имеющими не более одного удовлетворяющего присваивания. Эта задача также называется USAT. Алгоритму решения для UNAMBIGUOUS SAT разрешено демонстрировать любое поведение, включая бесконечные циклы, для формулы, имеющей несколько удовлетворяющих присваиваний. Хотя эта задача кажется проще, Валиант и Вазирани показали, что если существует практичный (т.е. рандомизированный полиномиальный) алгоритм для ее решения, то все задачи в NP могут быть решены так же легко. MAX SAT, задача максимальной выполнимости, является обобщением SAT в классе FNP. Она требует найти максимальное количество клауз, которые могут быть удовлетворены любым присваиванием. Для нее существуют эффективные алгоритмы аппроксимации, но точное решение является NP-трудным. Более того, она является APX-полной, что означает, что для этой задачи не существует полиномиальной схемы аппроксимации (PTAS), если только P=NP. WMSAT – это задача поиска присваивания минимального веса, удовлетворяющего монотонной булевой формуле (т.е. формуле без отрицаний). Веса пропозициональных переменных задаются во входных данных задачи. Вес присваивания – это сумма весов истинных переменных. Эта задача является NP-полной (см. теорему 1). Другие обобщения включают выполнимость для логики первого и второго порядка, задачи удовлетворения ограничениям, целочисленное линейное программирование.

Алгоритмы решения задачи SAT

Поскольку задача SAT является NP-полной, для неё известны только алгоритмы с экспоненциальной сложностью в худшем случае. Несмотря на это, эффективные и масштабируемые алгоритмы для SAT были разработаны в 2000-х годах и способствовали значительному прогрессу в нашей способности автоматически решать экземпляры задач, включающие десятки тысяч переменных и миллионы ограничений (то есть дизъюнктов). Примеры таких задач в автоматизированном проектировании электронных схем (EDA) включают формальную проверку эквивалентности, верификацию моделей, формальную верификацию конвейерных микропроцессоров, задачи планирования и составления расписаний и так далее. Механизм решения задач SAT также считается важным компонентом в инструментарии автоматизированного проектирования электронных схем. Основные методы, используемые современными решателями SAT, включают алгоритм Дэвиса–Путнама–Логеманна–Ловеленда (или DPLL), обучение на основе конфликтов (CDCL) и стохастические алгоритмы локального поиска, такие как WalkSAT. Почти все решатели SAT включают ограничение по времени выполнения, поэтому они завершатся за разумное время, даже если не смогут найти решение. Разные решатели SAT могут находить разные экземпляры задач простыми или сложными, и некоторые преуспевают в доказательстве выполнимости, а другие – в поиске решений. Предпринимались недавние попытки определить выполнимость экземпляра задач с использованием методов глубокого обучения. Решатели SAT разрабатываются и сравниваются на соревнованиях по решению задач SAT. Современные решатели SAT также оказывают значительное влияние на области верификации программного обеспечения, решения задач ограничений в искусственном интеллекте и исследования операций, среди прочего.