×

zbMATH — the first resource for mathematics

Skolem functions for DQBF. (English) Zbl 1398.68487
Artho, Cyrille (ed.) et al., Automated technology for verification and analysis. 14th international symposium, ATVA 2016, Chiba, Japan, October 17–20, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-46519-7/pbk; 978-3-319-46520-3/ebook). Lecture Notes in Computer Science 9938, 395-411 (2016).
Summary: We consider the problem of computing Skolem functions for satisfied dependency quantified Boolean formulas (DQBFs). We show how Skolem functions can be obtained from an elimination-based DQBF solver and how to take preprocessing steps into account. The size of the Skolem functions is optimized by don’t-care minimization using Craig interpolants and rewriting techniques. Experiments with our DQBF solver HQS show that we are able to effectively compute Skolem functions with very little overhead compared to the mere solution of the formula.
For the entire collection see [Zbl 1346.68003].
MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
ABC; CAQE; DepQBF
PDF BibTeX XML Cite
Full Text: DOI