@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@inproceedings{rabe-sat16,
  author    = {Markus N. Rabe and Sanjit A. Seshia},
  title     = {Incremental Determinization},
 booktitle = {Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT)},
 month = "July",
 year = {2016},
 pages = {375--392},
 abstract = {We present a novel approach to solve quantified boolean formulas 
with one quantifier alternation (2QBF). The algorithm incrementally 
adds new constraints to the formula until the constraints describe 
a unique Skolem function - or until the absence of a Skolem function 
is detected. Backtracking is required if the absence of Skolem functions 
depends on the newly introduced constraints. We present the algorithm 
in analogy to search algorithms for SAT and explain how propagation, 
decisions, and conflicts are lifted from values to Skolem functions. The 
algorithm improves over the state of the art in terms of the number of 
solved instances, solving time, and the size of the certificates.},
}