  We propose a new decision procedure for dependency quantified Boolean
formulas (DQBF) that uses interpolation-based definition extraction to compute
Skolem functions in a counter-example guided inductive synthesis (CEGIS) loop.
In each iteration, a family of candidate Skolem functions is tested for
correctness using a SAT solver, which either determines that a model has been
found, or returns an assignment of the universal variables as a counterexample.
Fixing a counterexample generally involves changing candidates of multiple
existential variables with incomparable dependency sets. Our procedure
introduces auxiliary variables -- which we call arbiter variables -- that each
represent the value of an existential variable for a particular assignment of
its dependency set. Possible repairs are expressed as clauses on these
variables, and a SAT solver is invoked to find an assignment that deals with
all previously seen counterexamples. Adding arbiter variables defines the
values of Skolem functions for assignments where they were previously
undefined, and may lead to the detection of Skolem functions by definition
extraction in subsequent iterations. A key feature of the proposed procedure is
that it is certifying by design: for true DQBF, models can be returned at
minimal overhead. Towards certification of false formulas, we prove that
clauses can be derived in an expansion-based proof system for DQBF. In an
experimental evaluation on standard benchmark sets, an implementation was able
to match (and in some cases, surpass) the performance of state-of-the-art DQBF
solvers. Moreover, models could be generated and validated for all true
instances that were solved.
