par-pd-depqbf
| 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) 694–707 | ||
| Results: | |||