Submitter: Florian Lonsing
Description: Devised by C. Jordan, L. Kaiser, F. Lonsing, and M. Seidl, this solver dynamically creates budgeted subproblems by setting outermost variables. The subproblems are solved using depqbf and its support for assumptions.
Details are available in
Jordan, C., Kaiser, L., Lonsing, F., Seidl, M.: MPIDepQBF: towards parallel QBF solving without knowledge sharing. In: International Conference on Theory and Applications of Satisfiability Testing, Springer (2014) 430437