2QBF: Challenges and Solutions
| Autor: | Valeriy Balabanov, Jie-Hong R. Jiang, Alan Mishchenko, Christoph Scholl, Robert K. Brayton |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Discrete mathematics
Range (mathematics) True quantified Boolean formula 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Graph theory 02 engineering and technology Certification Conjunctive normal form formula Disjunctive normal form Conjunctive normal form 020202 computer hardware & architecture Mathematics |
| Zdroj: | Theory and Applications of Satisfiability Testing – SAT 2016 ISBN: 9783319409696 SAT |
| DOI: | 10.1007/978-3-319-40970-2_28 |
| Popis: | 2QBF is a special form \(\forall \varvec{x} \exists \varvec{y}.\phi \) of the quantified Boolean formula (QBF) restricted to only two quantification layers, where \(\phi \) is a quantifier-free formula. Despite its restricted form, it provides a framework for a wide range of applications, such as artificial intelligence, graph theory, synthesis, etc. In this work, we overview two main 2QBF challenges in terms of solving and certification. We contribute several improvements to existing solving approaches and study how the corresponding approaches affect certification. We further conduct an extensive experimental comparison on both competition and application benchmarks to demonstrate strengths of the proposed methodology. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|