Булева проблема выполнимости
В логике и информатике проблема булевой выполнимости (иногда называемая пропозициональной проблемой выполнимости и сокращенно SATISFIABILITY , SAT или B-SAT ) — это проблема определения того, существует ли интерпретация , которая удовлетворяет данной булевой формуле . Другими словами, он спрашивает, можно ли последовательно заменить переменные данной логической формулы значениями ИСТИНА или ЛОЖЬ таким образом, чтобы формула оценивалась как ИСТИНА. В этом случае формула называется выполнимой. С другой стороны, если такого присвоения не существует, функция, выраженная формулой, ЛОЖЬ для всех возможных присвоений переменных, и формула невыполнима . Например, формула « а И НЕ b » выполнима, потому что можно найти значения а = ИСТИНА и b = ЛОЖЬ, которые делают ( а И НЕ b ) = ИСТИНА. Напротив, « а И НЕ а » невыполнимо.
SAT — первая задача, для которой было доказано, что она является NP-полной ; см . теорему Кука – Левина . Это означает, что все задачи класса сложности NP , который включает в себя широкий спектр естественных задач решения и оптимизации, в лучшем случае так же сложны для решения, как и SAT. Не существует известного алгоритма, который эффективно решает каждую задачу SAT, и обычно считается, что такого алгоритма не существует; тем не менее, это убеждение не было доказано математически, и решение вопроса о том, имеет ли SAT алгоритм с полиномиальным временем , эквивалентно проблеме P против NP , которая является известной открытой проблемой в теории вычислений.
Тем не менее, по состоянию на 2007 год эвристические SAT-алгоритмы способны решать экземпляры задач, включающие десятки тысяч переменных и формул, состоящих из миллионов символов, [1] чего достаточно для многих практических задач SAT, например, искусственного интеллекта , проектирования схем. , [2] и автоматическое доказательство теорем .
Формула пропозициональной логики , также называемая булевым выражением , строится из переменных , операторов И ( союз , также обозначаемый ∧), ИЛИ ( дизъюнкция , ∨), НЕ ( отрицание , ¬) и круглых скобок. Говорят, что формула выполнима , если ее можно сделать ИСТИННОЙ, присвоив соответствующие логические значения (т.е. ИСТИНА, ЛОЖЬ) ее переменным. Задача булевой выполнимости (SAT) состоит в том, чтобы по заданной формуле проверить, выполнима ли она. Эта проблема принятия решений имеет центральное значение во многих областях компьютерных наук , в том числетеоретическая информатика , теория сложности , [3] [4] алгоритмика , криптография [5] [6] и искусственный интеллект . [7] [ необходимы дополнительные ссылки ]
Литерал — это либо переменная, называемая положительным литералом , либо отрицание переменной, называемое отрицательным литералом . Предложение — это дизъюнкция литералов (или одного литерала). Предложение называется предложением Хорна, если оно содержит не более одного положительного литерала. Формула находится в конъюнктивной нормальной форме (CNF), если она является конъюнкцией предложений (или одного предложения). Например, 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 ) ∧ ИСТИНА и, в свою очередь, ИСТИНА ∧ ИСТИНА ∧ ИСТИНА (т.е. ИСТИНА). Напротив, формула КНФ a ∧ ¬ a, состоящее из двух предложений одного литерала, невыполнимо, так как для = ИСТИНА или = ЛОЖЬ оно оценивается как ИСТИНА ∧ ¬ИСТИНА (т. е. ЛОЖЬ) или ЛОЖЬ ∧ ¬ЛОЖЬ (т. е. снова ЛОЖЬ) соответственно.
