Relevance for SAT(ID)

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussavertaisarvioitu

Tutkijat

  • Joachim Jansen
  • Bart Bogaerts

  • Jo Devriendt
  • Gerda Janssens
  • Marc Denecker

Organisaatiot

Kuvaus

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.

Yksityiskohdat

AlkuperäiskieliEnglanti
OtsikkoProceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, {IJCAI} 2016
TilaJulkaistu - 2016
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaInternational Joint Conference on Artificial Intelligence - New York Hilton Midtown, New York, Yhdysvallat
Kesto: 9 heinäkuuta 201615 heinäkuuta 2016
Konferenssinumero: 25
http://ijcai-16.org/index.php/welcome/view/home

Conference

ConferenceInternational Joint Conference on Artificial Intelligence
LyhennettäIJCAI
MaaYhdysvallat
KaupunkiNew York
Ajanjakso09/07/201615/07/2016
www-osoite

ID: 6777791