Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями

Дано: формула F в КНФ, содержащая n переменных, m дизъюнктов и l литералов.

Требуется: выдать «Да», если для F имеется присваивание, обеспечивающее выполнимость формулы, т. е. подстановку булевых значений переменных, с которой значение F становится истинным, и «Нет» в противном случае.

Границы времени выполнения алгоритмов SAT, таким образом, можно выразить в форме <math>|F|^{O(1)} \cdot \alpha^n, |F|^{O(1)} \cdot \beta^m</math> или <math>|F|^O(1) \cdot \gamma^l</math>, где |F| – длина удовлетворительного битового представления F (т. е. формальных входных данных алгоритма). Фактически для существущих алгоритмов базы <math>\beta</math> и <math>\gamma</math> являются константами, а <math>\alpha</math> – функцией <math>\alpha(n, m)</math> от параметров формулы (поскольку не известно константы лучше <math>\alpha = 2</math>).