|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ИНХС РАН |
||
On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variablesстатья
Информация о цитировании статьи получена из
Scopus
Дата последнего поиска статьи во внешних источниках: 20 мая 2019 г.
- Авторы: Itsykson D., Knop A., Romashchenko A., Sokolov D.
- Сборник: 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)
- Том: 66
- Год издания: 2017
- Первая страница: 43:1
- Последняя страница: 43:14
- DOI: 10.4230/LIPIcs.STACS.2017.43
- Аннотация: Пан и Варди в 2004 году предложили подход к решению задачи выполнимости булевой формулы, названный ими символьной элиминацией кванторов. Подход состоит в последовательном присоединении частей формулы к OBDD (двоичной диаграмме разрешения с упорядоченными переменными). При этом всякий раз, когда к в диаграмму включены все члены формулы, содержащие некоторую переменную, применяется операция элиминации квантора (по данной переменной). Выполнимость исходной формулы легко определить по итоговой OBDD. Таким образом, сложность доказательства или опровержения формулы сводится к сложности процедуры преобразования формулы в OBDD. В общем случае сложность данной процедуры экспоненциальна (алгоритм работает экспоненциальное время на некоторых невыполнимых формулах -- это следует из общих оценок на связанные системы доказательств, полученные Сегерлиндом и Крайчеком). Однако выполнимые формулы интереснее с практической точки зрения и часто часто оказываются проще для различных типов SAT-солверов. В данной работе мы доказываем экспоненциальную нижнюю оценку на время работы таких алгоритмов на естественном классе выполнимых формулах. Трудная формула представляет собой систему линейных уравнений, представляющую проверочную матрицы некоторого кода, исправляющего ошибки. In 2004 Atserias, Kolaitis and Vardi proposed OBDD-based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of identically false OBDD from OBDDs representing clauses of the initial formula. All OBDDs in such proofs have the same order of variables. We initiate the study of OBDD based proof systems that additionally contain a rule that allows to change the order in OBDDs. At first we consider a proof system OBDD(and, reordering) that uses the conjunction (join) rule and the rule that allows to change the order. We exponentially separate this proof system from OBDD(and)-proof system that uses only the conjunction rule. We prove two exponential lower bounds on the size of OBDD(and, reordering)-refutations of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for OBDD(and)-proofs and the second one extends the result of Tveretina et al. from OBDD(and) to OBDD(and, reordering). In 2004 Pan and Vardi proposed an approach to the propositional satisfiability problem based on OBDDs and symbolic quantifier elimination (we denote algorithms based on this approach as OBDD(and, exists)-algorithms. We notice that there exists an OBDD(and, exists)-algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time. In contrast, we show that there exist formulas representing systems of linear equations over F_2 that are hard for OBDD(and, exists, reordering)-algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over F_2 that correspond to some checksum matrices of error correcting codes.
- Добавил в систему: Верещагин Николай Константинович