Learning for quantified boolean logic satisfiability

Abstract

Learning, i.e., the ability to record and exploit some informa-
\ntion which is unveiled during the search, proved to be a very
\neffective AI technique for problem solving and, in particular,
\nfor constraint satisfaction. We introduce learning as a general
\npurpose technique to improve the performances of decision
\nprocedures for Quantified Boolean Formulas (QBFs). Since
\nmany of the recently proposed decision procedures for QBFs
\nsolve the formula using search methods, the addition of learn-
\ning to such procedures has the potential of reducing useless
\nexplorations of the search space. To show the applicability
\nof learning for QBF satisfiability we have implemented it in
\nQ U BE, a state-of-the-art QBF solver. While the backjump-
\ning engine embedded in Q U BE provides a good starting point
\nfor our task, the addition of learning required us to devise new
\ndata structures and led to the definition and implementation of
\nnew pruning strategies. We report some experimental results
\nthat witness the effectiveness of learning. Noticeably, Q U BE
\naugmented with learning is able to solve instances that were
\npreviously out if its reach. To the extent of our knowledge,
\nthis is the first time that learning is proposed, implemented
\nand tested for QBFs satisfiability.