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...

Descripción completa

Detalles Bibliográficos
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