We study the symbolic approach to the propositional satisfiability problem proposed by Aguirre and Vardi in 2001 based on OBDDs and symbolic quantifier elimination. We study the theoretical limitations of the most general version of this approach where it is allowed to dynamically change variable order in OBDD. We refer to algorithms based on this approach as OBDD(∧,∃,reordering) algorithms. We prove the first exponential lower bound of OBDD(∧,∃,reordering) algorithms on unsatisfiable formulas, and give an example of formulas having short tree-like resolution proofs that are exponentially hard for OBDD(∧,∃,reordering) algorithms. We also present the first exponential lower bound for natural formulas with clear combinatorial meaning: every OBDD(∧,∃,reordering) algorithm runs exponentially long on the binary pigeonhole principle BPHPnn+1 © 2024 Elsevier B.V., All rights reserved.
Язык оригиналаАнглийский
DOI
СостояниеОпубликовано - 2024
Событие27th International Conference on Theory and Applications of Satisfiability Testing - , Индия
Продолжительность: 21 авг 202424 авг 2024

конференция

конференция27th International Conference on Theory and Applications of Satisfiability Testing
Сокращенное названиеSAT 2024
Страна/TерриторияИндия
Период21/08/2424/08/24

ID: 143425333