Abstract
Many solvers have been designed for QBFs, the validity problem for Quantified Boolean Formulas for the past few years. In this paper, we describe a new branching heuristics whose purpose is to promote renamable Horn formulas. This heuristics is based on Hébrard's algorithm for the recognition of such formulas. We present some experimental results obtained by our QBF solver Qbfl with the new branching heuristics and show how its performances are improved. © Springer-Verlag Berlin Heidelberg 2005.
Cite
CITATION STYLE
Coste-Marquis, S., Le Berre, D., & Letombe, F. (2005). A branching heuristics for quantified renamable Horn formulas. In Lecture Notes in Computer Science (Vol. 3569, pp. 393–399). Springer Verlag. https://doi.org/10.1007/11499107_30
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
