# Understanding and Extending Incremental Determinization for 2QBF

arXiv: https://arxiv.org/abs/1905.13411 · HTML: https://mlsanity.com/paper/1905.13411/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 May 2019.

## Built on by (most cited first, 4 of 4)

- [Engineering an Efficient Boolean Functional Synthesis Engine](https://mlsanity.com/paper/2108.05717/) (2021)
- [A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis](https://mlsanity.com/paper/2104.14098/) (2021)
- [Program Synthesis as Dependency Quantified Formula Modulo Theory](https://mlsanity.com/paper/2105.09221/) (2021)
- [Synthesis with Explicit Dependencies](https://mlsanity.com/paper/2301.10556/) (2023)

## Abstract (arXiv)

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.