---
title: "Relevance for SAT(ID)"
authors:
  - "Joachim Jansen"
  - "Bart Bogaerts"
  - "Jo Devriendt"
  - "Gerda Janssens"
  - "Marc Denecker"
doi: ""
url: "https://ijcai.org/proceedings/2016/91"
pdf: "https://ijcai.org/proceedings/2016/0091.pdf"
venue: "Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence"
year: 2016
pages: "596-601"
track: ""
keywords:
---

# Relevance for SAT(ID)

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

*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.