Laddar...
How QBF Expansion Makes Strategy Extraction Hard
In this paper we show that the QBF proof checking format QRAT (Quantified Resolution Asymmetric Tautologies) by Heule, Biere and Seidl cannot have polynomial time strategy extraction unless P=PSPACE. In our proof, the crucial property that makes strategy extraction PSPACE-hard for this proof format...
Sparad:
| I publikationen: | Automated Reasoning |
|---|---|
| Huvudupphovsmän: | , |
| Materialtyp: | Artigo |
| Språk: | Inglês |
| Publicerad: |
2020
|
| Ämnen: | |
| Länkar: | https://ncbi.nlm.nih.gov/pmc/articles/PMC7324150/ https://ncbi.nlm.nih.govhttp://dx.doi.org/10.1007/978-3-030-51074-9_5 |
| Taggar: |
Lägg till en tagg
Inga taggar, Lägg till första taggen!
|