资源Solving QBF by Clause Selection?

Solving QBF by Clause Selection?

2019-11-18 | |  32 |   1 |   0
Abstract Algorithms based on the enumeration of implicit hitting sets find a growing number of applications, which include maximum satisfiability and model based diagnosis, among others. This paper exploits enumeration of implicit hitting sets in the context of Quantified Boolean Formulas (QBF). The paper starts by developing a simple algorithm for QBF with two levels of quantification, which is shown to relate with existing work on enumeration of implicit hitting sets, but also with recent work on QBF based on abstraction refinement. The paper then extends these ideas and develops a novel QBF algorithm, which generalizes the concept of enumeration of implicit hitting sets. Experimental results, obtained on representative problem instances, show that the novel algorithm is competitive with, and often outperforms, the state of the art in QBF solving.

上一篇:Expressive Logical Combinators for Free Pierre Geneve?s Alan Schmitt?

下一篇:Towards Automatic Dominance Breaking for Constraint Optimization Problems?

用户评价
全部评价

热门资源

  • Multi-Source Cros...

    Modern NLP applications have enjoyed a great bo...

  • Reference Network...

    Neural Machine Translation (NMT) has achieved n...

  • Soft Contextual D...

    While data augmentation is an important trick t...

  • Style Transformer...

    Disentangling the content and style in the lat...

  • Towards Fine-grai...

    In this paper, we focus on the task of finegra...