Solving QBF by Abstraction

Many verification and synthesis approaches rely on solving techniques for quantified Boolean formulas (QBF). Consequently, solution witnesses, in the form of Boolean functions, become more and more important as they represent implementations or counterexamples. We present a recursive counterexample...

Full description

Bibliographic Details
Main Authors: Jesko Hecking-Harbusch, Leander Tentrup
Format: Article
Language:English
Published: Open Publishing Association 2018-09-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1604.06752v2