Построение алгоритмов для задач булевой логики

Интерес к доказательству экспоненциальных верхних оценок для NP-трудных задач в последние несколько десятилетий остается на стабильно высоком уровне. Одним из наиболее хорошо изученных подходов к доказательству таких оценок является метод расщепления. Впервые данный метод был предложен в 1960 году Дэвисом и Патнемом и сформулирован в более современном виде Дэвисом, Лоджеманном и Лавлэндом 1962 году. Его основная идея заключается в расщеплении входного примера задачи на несколько более простых примеров, таких что, построив решение для каждого из них, возможно за полиномиальное время построить решение для исходного примера. В работе приводятся несколько новых подходов к разработке и анализу алгоритмов расщепления для задач булевой логики. Описывается компьютерная программа для автоматического анализа времени работы таких алгоритмов. Также показывается, как с помощью использования запоминания дизъюнктов и комбинированных мер сложности получать более сильные верхние оценки на время работы.