4446
правок
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями
Материал из WEGA
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида (посмотреть исходный код)
Версия от 15:19, 18 июня 2020
, 18 июня 2020→Постановка задачи
Irina (обсуждение | вклад) (Новая страница: «== Ключевые слова и синонимы == Задача выполнимости булевых формул (SAT) == Постановка задач…») |
Irina (обсуждение | вклад) |
||
| Строка 6: | Строка 6: | ||
Задача 1 (SAT). Дано: формула F в КНФ, содержащая n переменных, m дизъюнктов clauses и l литералов. | '''Задача 1 (SAT).''' | ||
Дано: формула F в КНФ, содержащая n переменных, m дизъюнктов clauses и l литералов. | |||
Требуется: выдать «Да», если F содержит присваивание, обеспечивающее выполнимость формулы, т. е. подстановку булевых значений переменных, с которой значение F становится истинным, и «Нет» в противном случае. | Требуется: выдать «Да», если F содержит присваивание, обеспечивающее выполнимость формулы, т. е. подстановку булевых значений переменных, с которой значение F становится истинным, и «Нет» в противном случае. | ||
Границы времени выполнения алгоритмов SAT, таким образом, можно выразить в форме |F|O(1) | Границы времени выполнения алгоритмов 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>). | ||
== Нотация == | == Нотация == | ||
