QuBE7.0

In this paper we outline QuBE7's main features, describing first the options of the preprocessors, and then giving some details about how the core search-based solver (i) performs unit and pure literal propagation; and (ii) performs the "Conflict Analysis procedure" for non-chronological backtracking, generalised from the SAT to the QBF case. We conclude with the experimental evaluation, showing that QuBE7.0 is the a state-of-the-art single-engine QBF solver.

• Type: Journal
• Year: 2010
• Where: JSAT
• Authors: Enrico Giunchiglia, Paolo Marin, Massimo Narizzano
• Keywords: Core Search-based Solver, JSAT 2010, Pure Literal Propagation, Single-engine Qbf Solver