Steklov Institute of Mathematics at St.Petersburg

PREPRINT 01/2014

LOWER BOUNDS FOR DPLL ALGORITHMS WITH SPLITTING OVER LINEAR FUNCTIONS

This preprint was accepted January 10, 2014

ABSTRACT:
A typical DPLL algorithm for the Boolean satisfiability problem splits the input
problem into two by assigning the two possible values to a variable; then it
simplifies the resulting two formulas. There are more complicated forms of splitting
(for example, splitting by a clause), but they are usually reducible to splitting
over a single variable. DPLL algorithms form the base of most modern SAT solvers,
and there is a significant interest in exponential lower bounds for them.

In this paper we consider an extension of the DPLL paradigm. Our algorithms,
DPLL_lin, can split over arbitrary linear function modulo two. These algorithms
quickly solve formulas that encode linear systems modulo two, which were used for
proving exponential lower bounds for conventional DPLL algorithms.

We prove exponential lower bounds on the running time of DPLL_lin
algorithms. Moreover, we extend the concept of these algorithms to two newly
constructed proof systems ResL and SemL and prove exponential lower bounds on
the size of tree-like proofs in these systems.

 

Д. О. Соколов

НИЖНИЕ ОЦЕНКИ НА ВРЕМЯ РАБОТЫ DPLL АЛГОРИТМОВ С РАСЩЕПЛЕНИЕМ ПО ЛИНЕЙНЫМ ФУНКЦИЯМ

АННОТАЦИЯ
В данной работе рассматривается усиленная версия DPLL алгоритмов для решения
задачи выполнимости булевых формул~--- DPLL_lin алгоритмы. Мы разрешаем алгоритмы
производить расщепление по линейным функциям над полем F_2, и докажем, что
при этом мы сможем определить выполнимость булевой формулы, кодирующей линейную
систему уравнений за полиномиальное время, в отличие от классических DPLL
алгоритмов, для которых на указанных формулах достигается экспоненциальная оценка.

Экспоненциальные нижние оценки на время время работы классических DPLL алгоритмов
на невыполнимых формулах следуют из нижних оценок на размер резолюционных
доказательств. Мы предложим новые системы доказательств ResL и SemL, связанные с
DPLL_lin алгоритмами. И докажем нижние оценки на tree-like версию данных систем, как
следствие мы получим явную серию примеров невыполнимых формул, на которых достигается
экспоненциальная нижняя оценка на время работы DPLL_lin алгоритмов.