Incremental Determinization

Markus N. Rabe and Sanjit A. Seshia. Incremental Determinization. In Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 375–392, July 2016.

Download

[pdf] 

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.

BibTeX

@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.},
}