Katalin Fazekas, Marijn Heule, Martina Seidl, Armin Biere,
"Skolem Function Continuation for Quantified Boolean Formulas"
, in Sebastian Gabmeyer and Einar Broch Johnsen: Tests and Proofs - 11th International Conference, TAP 2017, Held as Part of STAF 2017, Marburg, Germany, July 19-20, 2017, Proceedings, Serie Lecture Notes in Computer Science, Vol. 10375, Springer, Seite(n) 129--138, 2017
Skolem Function Continuation for Quantified Boolean Formulas
Sprache des Titels:
Tests and Proofs - 11th International Conference, TAP 2017, Held as Part of STAF 2017, Marburg, Germany, July 19-20, 2017, Proceedings
Modern solvers for quantified Boolean formulas (QBF) not only decide the satisfiability of a formula, but also return a set of Skolem functions representing a model for a true QBF. Unfortunately, in combination with a preprocessor this ability is lost for many preprocessing techniques. A preprocessor rewrites the input formula to an equi-satisfiable formula which is often easier to solve than the original formula. Then the Skolem functions returned by the solver represent a solution for the preprocessed formula, but not necessarily for the original encoding.
Our solution to this problem is to combine Skolem functions obtained from a ????????
trace as produced by the widely-used preprocessor Bloqqer with Skolem functions for the preprocessed formula. This approach is agnostic of the concrete rewritings performed by the preprocessor and allows the combination of Bloqqer with any Skolem function producing solver, hence realizing a smooth integration into the solving tool chain.