Understanding and Extending Incremental Determinization for 2QBF

Markus Rabe, Leander Tentrup, Cameron Rasmussen, and Sanjit A. Seshia. Understanding and Extending Incremental Determinization for 2QBF. In 30th International Conference on Computer Aided Verification (CAV), 2018.

Download

[pdf] 

Abstract

Incremental determinization is a recently proposed algorithm for solving quantified Boolean formulas with one quantifier alternation. In this paper, we formalize incremental determinization as a set of inference rules to help understand the design space of similar algorithms. We then present additional inference rules that extend incremental determinization in two ways. The first extension integrates the popular CEGAR principle and the second extension allows us to analyze different cases in isolation. The experimental evaluation demonstrates that the extensions significantly improve the performance.

BibTeX

@inproceedings{rabe-cav18,
  author = {Markus Rabe and Leander Tentrup and Cameron Rasmussen and Sanjit A. Seshia},
  title = {Understanding and Extending Incremental Determinization for 2QBF},
  booktitle = {30th International Conference on Computer Aided Verification (CAV)},
  year = {2018},
  abstract = {Incremental determinization is a recently proposed algorithm 
for solving quantified Boolean formulas with one quantifier alternation. 
In this paper, we formalize incremental determinization as a set of inference 
rules to help understand the design space of similar algorithms. 
We then present additional inference rules that extend incremental determinization 
in two ways. The first extension integrates the popular 
CEGAR principle and the second extension allows us to analyze different 
cases in isolation. The experimental evaluation demonstrates that 
the extensions significantly improve the performance.},
}