Cargando…
Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness
In applications, QBF solvers are expected to not only decide whether a given formula is true or false but also return a solution in the form of a strategy. Determining whether strategies can be efficiently extracted from proof traces generated by QBF solvers is a fundamental research task. Most reso...
Autores principales: | Schlaipfer, Matthias, Slivovsky, Friedrich, Weissenbacher, Georg, Zuleger, Florian |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326563/ http://dx.doi.org/10.1007/978-3-030-51825-7_30 |
Ejemplares similares
-
Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing
por: Slivovsky, Friedrich
Publicado: (2020) -
Building Strategies into QBF Proofs
por: Beyersdorff, Olaf, et al.
Publicado: (2020) -
Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs
por: Schlaipfer, Matthias, et al.
Publicado: (2016) -
How QBF Expansion Makes Strategy Extraction Hard
por: Chew, Leroy, et al.
Publicado: (2020) -
Positional Games and QBF: The Corrective Encoding
por: Mayer-Eichberger, Valentin, et al.
Publicado: (2020)