|Description:|| Devised by Mikolas Janota, is an abstraction based solver, which performs a kind of resolution and expansion procedure but in a depth-first way, i.e., by expanding first only one value of a variable, and learns abstractions of the local partial solutions to refine the global solution. |
The submitted version includes bloqqer as preprocessor.
Details are available in
Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving qbf with counterexample guided refinement. In: Theory and Applications of Satisfiability Testing– SAT 2012, Springer Berlin Heidelberg (2012) 114–128