On computing generalized backbones

Alessandro Previti, Alexey Ignatiev, Matti Jarvisalo, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

1 Citation (Scopus)


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.

Original languageEnglish
Title of host publicationProceedings - 2017 International Conference on Tools with Artificial Intelligence - ICTAI 2017
EditorsMaria Virvou
Place of PublicationPiscataway NJ USA
PublisherIEEE, Institute of Electrical and Electronics Engineers
Number of pages7
ISBN (Electronic)9781538638767
ISBN (Print)9781538638774
Publication statusPublished - 2017
Externally publishedYes
EventInternational Conference on Tools with Artificial Intelligence 2017 - Boston, United States of America
Duration: 6 Nov 20178 Nov 2017
Conference number: 29th


ConferenceInternational Conference on Tools with Artificial Intelligence 2017
Abbreviated titleICTAI 2017
Country/TerritoryUnited States of America
Internet address


  • Backbone variables
  • Boolean satisfiability
  • Constraint satisfaction
  • Satisfiability Modulo Theories

Cite this