Title: QBF Resolution Systems and Their Proof Complexities
Abstract: Quantified Boolean formula (QBF) evaluation has a broad range of applications in computer science and is gaining increasing attention. Recent progress has shown that for a certain family of formulas, Q-resolution, which forms the foundation of learning in modern search-based QBF solvers, is exponentially inferior in proof size to two of its extensions: Q-resolution with resolution over universal literals (QU-resolution) and long-distance Q-resolution (LQ-resolution). The relative proof power between LQ-resolution and QU-resolution, however, remains unknown. In this paper, we show their incomparability by exponential separations on two families of QBFs, and further propose a combination of the two resolution methods to achieve an even more powerful proof system. These results may shed light on solver development with enhanced learning mechanisms. In addition, we show how QBF Skolem/Herbrand certificate extraction can benefit from polynomial LQ-resolution proofs in contrast to their exponential Q-resolution counterparts.
Publication Year: 2014
Publication Date: 2014-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 65
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot