| Description: | Devised by Paolo Marin, it is a search-based QBF solver for prenex conjunctive normal form (PCNF) formulas. Literal propagation is performed through unit, pure, and don't care literal detection using lazy data structures. For backtracking, a conflict and solution driven constraint learning approach is used. A restart strategy and phase saving are also implemented.
This version uses first semantic UIP (S-UIP) learning, 2 literals watching, and VSIDS decision heuristic.
The solver is coupled with the QBF preprocessor sQueezeBF, which is given a timeout of 100 seconds. | |
