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

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

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

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

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

• Например, формула "a AND NOT b" является выполнимой, потому что можно найти значения a = TRUE и b = FALSE, которые делают "a AND NOT b" ИСТИННЫМ.

• Напротив, "И-НЕ" невозможно выполнить.

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

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

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

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

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