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

Типичный алгоритм «разделяй и властвуй» для задачи SAT состоит из двух этапов: разбиение исходной задачи на несколько подзадач (например, редукция SAT(F) до SAT(F[x]) и SAT(F[:x])) и упрощение полученных подзадач при помощи правил преобразования с полиномиальным временем работы, не влияющих на выполнимость подзадач (т.е. заменяющих формулу другой формулой, в равной мере выполнимой). Подзадачи F1, ..., Fk для разбиения выбираются таким образом, чтобы соответствующее рекуррентное неравенство с упрощенными задачами F[,..., Fk0, к T(F) < X T(Fi0) + const ;