New Approaches to Boolean Quantifier Elimination

Efficient and adaptive EBQE techniques are furthermore well known to be vital especially in large-scale
industrial settings.  Among the applications we find e.g. the computation of Craig interpolants,
image computation in symbolic model checking, computing all counter examples, or counter example minimization.

First we present four different approaches to EBQE: variable elimination by clause distribution,
model enumeration with projection, DNNF computation with projection, and substitute \& simplify.  
We then present work in progress on a portfolio approach to combine these different algorithms and
choose the "best" algorithm depending on certain features of the (sub)-formula.