[Back]

F. Slivovsky:
"Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing";
Talk: International Conference on Computer Aided Verification (CAV), Los Angeles, USA; 2020-07-19 - 2020-07-24; in: "CAV 2020: Computer Aided Verification", LNCS, 12224 (2020), ISBN: 978-3-030-53287-1; 508 - 528.

We present a new semantic gate extraction technique for
propositional formulas based on interpolation. While known gate detection
methods are incomplete and rely on pattern matching or simple
semantic conditions, this approach can detect any definition entailed by
an input formula.
As an application, we consider the problem of computing unique strategy
functions from Quantified Boolean Formulas (QBFs) and Dependency
Quantified Boolean Formulas (DQBFs). Experiments with a prototype
implementation demonstrate that functions can be efficiently
extracted from formulas in standard benchmark sets, and that many
of these definitions remain undetected by syntactic gate detection.
We turn this into a preprocessing technique by substituting unique
strategy functions for input variables and test solver performance on the
resulting instances. Compared to syntactic gate detection, we see a significant
increase in the number of solved QBF instances, as well as a
modest increase for DQBF instances.

http://dx.doi.org/10.1007/978-3-030-53288-8_24

https://publik.tuwien.ac.at/files/publik_292443.pdf