资源论文Relevance for SAT(ID)

Relevance for SAT(ID)

2019-11-22 | |  64 |   36 |   0
Abstract 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.

上一篇:Truncating Shortest Path Search for Efficient Map-Matching

下一篇:Counting Linear Extensions of Sparse Posets?

用户评价
全部评价

热门资源

  • The Variational S...

    Unlike traditional images which do not offer in...

  • Learning to Predi...

    Much of model-based reinforcement learning invo...

  • Stratified Strate...

    In this paper we introduce Stratified Strategy ...

  • A Mathematical Mo...

    Direct democracy, where each voter casts one vo...

  • Rating-Boosted La...

    The performance of a recommendation system reli...