Relevance for SAT(ID)

Joachim Jansen, Bart Bogaerts, Jo Devriendt, Gerda Janssens, Marc Denecker

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

4 Citations (Scopus)


Inductive definitions and justifications are wellstudied concepts. Solvers that support inductive definitions have been developed, but several of their computationally nice properties have never been exploited to improve these solvers. In this paper, we present a new notion called relevance. We determine a class of literals that are relevant for a given definition and partial interpretation, and show that choices on irrelevant atoms can never benefit the search for a model. We propose an early stopping criterion and a modification of existing heuristics that exploit relevance. We present a first implementation in MinisatID and experimentally evaluate our approach, and study how often existing solvers make choices on irrelevant atoms.
Original languageEnglish
Title of host publicationProceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, {IJCAI} 2016
PublisherAAAI Press
Number of pages7
ISBN (Print)978-1-57735-770-4
Publication statusPublished - 2016
MoE publication typeA4 Conference publication
EventInternational Joint Conference on Artificial Intelligence - New York Hilton Midtown, New York, United States
Duration: 9 Jul 201615 Jul 2016
Conference number: 25


ConferenceInternational Joint Conference on Artificial Intelligence
Abbreviated titleIJCAI
Country/TerritoryUnited States
CityNew York
Internet address


Dive into the research topics of 'Relevance for SAT(ID)'. Together they form a unique fingerprint.

Cite this