Name
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. |
Year | Venue | DocType |
|---|---|---|
2016 | IJCAI | Conference |
Citations | PageRank | References |
0 | 0.34 | 13 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Joachim Jansen | 1 | 22 | 3.85 |
| Bart Bogaerts | 2 | 83 | 16.49 |
| Jo Devriendt | 3 | 10 | 5.76 |
| Gerda Janssens | 4 | 644 | 58.82 |
| Marc Denecker | 5 | 1626 | 106.40 |