Relevance for SAT(ID)

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

Relevance for SAT(ID)

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

Download BibTeX Cite

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence. Pages 596-601.

Abstract

Inductive definitions and justifications are well-studied 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.

Joachim Jansen, Bart Bogaerts, Jo Devriendt, Gerda Janssens, and Marc Denecker. 2016. Relevance for SAT(ID). In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16. IJCAI, 596–601. https://ijcai.org/proceedings/2016/91

@inproceedings{ijcai2016p91,
  title     = {Relevance for SAT(ID)},
  author    = {Jansen, Joachim and Bogaerts, Bart and Devriendt, Jo and Janssens, Gerda and Denecker, Marc},
  booktitle = {Proceedings of the Twenty-Fifth International Joint Conference on
               Artificial Intelligence, {IJCAI-16}},
  publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
  editor    = {Subbarao Kambhampati},
  pages     = {596--601},
  year      = {2016},
  month     = {7},
  url       = {https://ijcai.org/proceedings/2016/91},
}

TY  - CPAPER
TI  - Relevance for SAT(ID)
AU  - Jansen, Joachim
AU  - Bogaerts, Bart
AU  - Devriendt, Jo
AU  - Janssens, Gerda
AU  - Denecker, Marc
T2  - Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16
PB  - AAAI Press / International Joint Conferences on Artificial Intelligence
PY  - 2016
SP  - 596
EP  - 601
UR  - https://ijcai.org/proceedings/2016/91
ER  -