Страница публикации
On Computing Generalized Backbones
Тип публикации: Материал конференции
Тип материала: Текст
Авторы: Previti A., Jarvisalo M., Marques-Silva J., Ignatiev A.
Журнал: Proc. 29th IEEE Intern. Conf. on Tools with Artificial Intelligence (ICTAI 29, Boston, MA, 06-08 ноября 2017 г.)
Язык публикации: english
Номера страниц: 1050-1056
Количество страниц: 7
Год публикации: 2018
Отчетный год: 2018
Издательство: IEEE Computer Society
Название издательства: IEEE Computer Society
Аннотация: The concept of backbone variables, i.e., variables that take the same value in all solutions-or, equivalently, never take a specific value-finds various important applications in the context of Boolean satisfiability (SAT), motivating the development of efficient algorithms for determining the set of backbone variables of a given propositional formula. Notably, this problem surpasses the complexity of merely deciding satisfiability. In this work we consider generalizations of the concept of backbones in SAT to non-binary (and potentially infinite) domain constraint satisfaction problems. Specifically, we propose a natural generalization of backbones to the context of satisfiability modulo theories (SMT), applicable to a range of different theories as well as CSPs in general, and provide two generic algorithms for determining the backbone in this general context. As two concrete instantiations, we focus on two central SMT theories, the theory of linear integer arithmetic (LIA) with infinite integer domains, and the theory of bit vectors (BV), and empirically evaluate the potential of the proposed algorithms on both LIA and BV instances.
Индексируется WOS: Нет
Индексируется Scopus: Нет
Индексируется УБС: Нет
Индексируется РИНЦ: Да
Индексируется ВАК: Нет
Индексируется CORE: Нет
Export Citations