Описание тега satisfiability

Описание тега Вопросы с тегом

Выполнимость (часто пишется заглавными буквами или сокращенно SAT) - это проблема определения, можно ли присвоить переменным данной булевой формулы таким образом, чтобы формула оценивалась как ИСТИНА.

В основном из Википедии:

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

Другими словами, он спрашивает, можно ли последовательно заменить переменные данной логической формулы значениями true или false таким образом, что формула оценивается как true.

Если это так, формула называется satisfiable. С другой стороны, если такого присвоения не существует, функция, выраженная формулой, идентичноfalse для всех возможных назначений переменных и формула unsatisfiable.

For example, the formula "*a AND NOT b*" is satisfiable 
because one can find the values a = TRUE and b = FALSE, 
which make (a AND NOT b) = TRUE. 

In contrast, (a AND NOT a) is unsatisfiable.

SAT- одна из первых задач, NP-завершенность которой доказана. Это означает, что все проблемы вcomplexity class NP, который включает в себя широкий спектр естественных решений и задач оптимизации, в техническом смысле так же сложно решить, как и SAT.

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

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

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

В настоящее время исследования по теории SAT продолжаются, если вы хотите быть в курсе этих исследований, посетите: http://www.satlive.org/.