Submitter: Florian Lonsing
Description: Devised by U. Egly, F. Lonsing, and J. Oetsch. In this solver, the approach to solve quantified circuits in prenex-normal form relies on running two instances of a QBF solver on a primal and a dual version of the problem encoding in parallel as described in [1]. par-pd-depqbf makes use of preprocessing by means of bloqqer, and it uses depqbf as back-end PCNF QBF solver.
[1] Van Gelder, A.: Primal and dual encoding from applications into quantified boolean formulas. In: International Conference on Principles and Practice of Constraint Programming, Springer (2013) 694707