QUBE-BJ

Submitter: Massimo Narizzano
Description: Devised by Enrico Giunchiglia, Massimo Narizzano e Armando Tacchella, it is a search-based solver written in C++ featuring lazy data structures for unit and pure literal propagation. QUBE-BJ features conflict and solution-directed backjumping. The heuristic is an extension to QBF of zChaff heuristic for SAT.[ E. Giunchiglia, M. Narizzano, and A. Tacchella. QuBE++ an Efficient QBF Solver. In 5th Formal Methods in Computer Aided Design conference (FMCAD 2004), Lecture Notes in Computer Science. Springer Verlag, 2004.]
Results: