K-КНФ-алгоритмы на основе поиска с возвратом: различия между версиями

Время выполнения ResolveSat(F, s, I) можно ограничить следующим образом. '''Resolve'''(F, s) добавляет не более <math>O(n^s) \;</math> дизъюнктов к F за счет сравнения пар дизъюнктов, так что прямолинейная реализация будет выполняться за время <math>n^{3s}poly(n) \;</math> (эту границу можно улучшить, однако ее улучшение не повлияет на асимптотику основного результата). '''Search'''(<math>F_s, \; I</math>) требует <math>I(|F| + n^s)poly(n) \;</math> времени. Следовательно, полное время выполнения '''ResolveSat'''(F, s, I) можно грубо ограничить сверху значением <math>(n^{3s} + I(|F| + n^s))poly(n) \;</math>. If s = O(n/log n), общее время выполнения можно ограничить значением <math>I|F|2^{O(n)} \;</math>, поскольку <math>n^s = 2^{O(n)} \;</math>. Для этого нужно взять в качестве s некоторую константу достаточно большой величины или ''медленно растущую'' функцию от n. Таким образом, s(n) будет стремиться к бесконечности с n, но будет оставаться в пределах O(log n).

Легко показать, что <math>\mu_3 = 4 - 4 \; ln \; 2 > 1,226</math>, используя разложение функции ln 2 в ряд Тейлора. Используя стандартные способы, также легко показать, что <math>\mu_k \;</math> представляет собой возрастающую функцию от k с пределом <math>\sum_{j=1}^{\infty} (1 / j^2) = (\pi^2 / 6) = 1,644</math>.