Sciweavers

SAT
2005
Springer

Local and Global Complete Solution Learning Methods for QBF

13 years 9 months ago
Local and Global Complete Solution Learning Methods for QBF
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 solutio...
Ian P. Gent, Andrew G. D. Rowley
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where SAT
Authors Ian P. Gent, Andrew G. D. Rowley
Comments (0)