Abstract Branching for Quantified Formulas

Marco Benedetti

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.

Subjects: 15.7 Search; 15.2 Constraint Satisfaction

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.