Local and global complete solution learning methods for QBF

I P Gent, A G D Rowley

Research output: Book/ReportBook

1 Citation (Scopus)

Abstract

Solvers for Quantified Boolean Formulae (QBF) use many analogues of technique from SAT. A significant amount of work has gone into extending conflict based techniques such as conflict learning to solution learning, which is irrelevant in SAT but can play a large role in success in QBF. Unfortunately, solution learning techniques have not been highly successful to date. We argue that one reason for this is that solution learning techniques have been 'incomplete'. That is, not all the information implied in a solution is learnt. We introduce two new techniques for learning as much as possible from solutions, and we call them complete methods. The two methods contrast in how long they keep information. One, Complete Local Solution Learning, discards solutions on backtracking past a previous existential variable. The other, Complete Global Solution Learning, keeps solutions indefinitely. Our detailed experimental analysis suggests that both can improve search over standard solution learning, while the local method seems to offer a more suitable tradeoff than global learning.

Original languageEnglish
PublisherUnknown Publisher
Number of pages16
Publication statusPublished - 2005

Fingerprint

Dive into the research topics of 'Local and global complete solution learning methods for QBF'. Together they form a unique fingerprint.

Cite this