# Understanding and Extending Incremental Determinization for 2QBF

## TL;DR

This paper formalizes and extends incremental determinization for 2QBF, integrating CEGAR and case analysis to improve solver performance, supported by experimental validation.

## Contribution

It introduces a formal set of inference rules for incremental determinization and proposes two novel extensions that enhance its effectiveness.

## Key findings

- Extensions significantly improve performance
- Formalization aids understanding of algorithm design space
- Experimental results validate the improvements

## 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.