Title
Learning for quantified boolean logic satisfiability
Abstract
Learning, i.e., the ability to record and exploit some information which is unveiled during the search, proved to be a very effective AI technique for problem solving and, in particular, for constraint satisfaction. We introduce learning as a general purpose technique to improve the performances of decision procedures for Quantified Boolean Formulas (QBFs). Since many of the recently proposed decision procedures for QBFs solve the formula using search methods, the addition of learning to such procedures has the potential of reducing useless explorations of the search space. To show the applicability of learning for QBF satisfiability we have implemented it in QUBE, a state-of-the-art QBF solver. While the backjumping engine embedded in QUBE provides a good starting point for our task, the addition of learning required us to devise new data structures and led to the definition and implementation of new pruning strategies. We report some experimental results that witness the effectiveness of learning. Noticeably, QUBE augmented with learning is able to solve instances that were previously out if its reach. To the extent of our knowledge, this is the first time that learning is proposed, implemented and tested for QBFs satisfiability.
Year
Venue
Keywords
2002
AAAI/IAAI
general purpose technique,effective ai technique,decision procedure,qbf satisfiability,search space,qbfs satisfiability,new data structure,state-of-the-art qbf solver,search method,boolean logic satisfiability,new pruning strategy,bayesian networks,constraint satisfaction,data structure,satisfiability
Field
DocType
ISBN
Constraint satisfaction,Data structure,Computer science,Satisfiability,Theoretical computer science,Bayesian network,Constraint learning,Artificial intelligence,Boolean algebra,Solver,Backjumping,Machine learning
Conference
0-262-51129-0
Citations 
PageRank 
References 
35
2.24
15
Authors
3
Name
Order
Citations
PageRank
Enrico Giunchiglia12380164.28
Massimo Narizzano245130.41
Armando Tacchella31448108.82