QBF Solver : ZDDs

[SSoelvsten]

The QBF benchmark lacks support for ZDDs. It should not be too difficult to extend the adapter for the final few things still missing; some of it is already done with the new Knight's Tour encoding.

Missing In ZDD Adapters

• ithvar(...)
• nithvar(...)
• ite(...)
• exists(...)
• forall(...)
• pickcube(...)

Other Tasks

• Negation seems possibly not the same as the Complement? one should only complement a subset of the variables; essentially leaving all the Don't Care domain variables as-is.
• The final quantifier block compares to adapter.top(). Yet, we cannot do so for ZDDs, since we have removed variables. The quick-n-dirty solution is to use an extend at the final quantifier block.