Talks and Poster Presentations (with Proceedings-Entry):
R. Bloem, N. Braud-Santoni, V. Hadzic, U. Egly, F. Lonsing, M. Seidl:
"Expansion-Based QBF Solving Without Recursion";
Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD),
Austin, TX, USA;
- 2018-11-02; in: "2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018",
In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over Boolean variables. Such approaches partially expand one type of variable (either existential or universal) and pass the obtained formula to a SAT solver for deciding the QBF. State-of-the-art expansion-based solvers process the given formula quantifier-block wise and recursively apply expansion until a solution is found.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.