Submitter: Florian Letombe
Description: Devised by Florian Letombe, it is a search-based solver written in C, packed with a number of features as trivial-truth, trivial-falsity, Horn and reverse-Horn formulas detection. QBFL is implemented on top of Limmat. QBFL-BS uses an extension of Bohm and Speckenmeyer's heuristic for SAT.