Preprocessing QBF
Principles and Practice of Constraint Programming(2006)
摘要
In this paper we investigate the use of preprocessing when solving Quantified Boolean Formulas (QBF). Many different problems can be efficiently encoded as QBF instances, and there has been a great deal of recent interest and progress in solving such instances efficiently. Ideas from QBF have also started to migrate to CSP with the exploration of Quantified CSPs which offer an intriguing increase in representational power over traditional CSPs. Here we show that QBF instances can be simplified using techniques related to those used for preprocess- ing SAT.These simplifications can be performed in polynomial time,and are used to preprocess the instance prior to invoking a worst case exponential algorithm to solve it. We develop a method for preprocessing QBF instances that is empiri- cally very effective. That is, the preprocessed formulas can be solved significantly faster, even when we account for the time required to perform the preprocessing. Our method significantly improves the efficiency of a range of state-of-the-art QBF solvers. Furthermore, our method is able to completely solve some instances just by preprocessing, including some instances that to our knowledge have never been solved before by any QBF solver.
更多查看译文
关键词
preprocessing QBF instance,state-of-the-art QBF solvers,traditional CSPs,Quantified Boolean Formulas,polynomial time,different problem,Quantified CSPs,preprocessing SAT,QBF solver,QBF instance,Preprocessing QBF
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络