Proceedings:
Proceedings of the AAAI Conference on Artificial Intelligence, 21
Volume
Issue:
Technical Papers
Track:
Constraint Satisfaction and Satisfiability
Downloads:
Abstract:
We introduce a novel search-based decision procedure for Quantified Boolean Formulas (QBFs), called Abstract Branching. As opposed to standard search-based procedures, it escapes the burdensome need for branching on both children of every universal node in the search tree. This is achieved by branching on existential variables only, while admissible universal assignments are inferred. Running examples and experimental results are reported.
AAAI
Technical Papers