|
Message passing for quantified Boolean formulas |
2012-02-10
Text Size:
A A A |
Institute of Theoretical Physics Chinese Academy of Sciences |
学术报告 |
Title 题目 |
Message passing for quantified Boolean formulas |
Speaker 报告人 |
张潘 博士 |
意大利都灵理工大学物理系 |
Date 日期 |
2012-02-10 PM 15:00 Friday |
Venue 地点 |
Conference Hall 322, ITP/理论物理所322报告厅 |
Abstract 摘要 |
Quantified Boolean Formulas problem(QBF) is a prototype problem that harder than NP. We propose two types of message passing algorithms for QBF. The first type is a message passing based heuristics that can prove unsatisfiability of the QBF by assigning the universal variables in such a way that the remaining formula is unsatisfiable. In the second type, we use message passing to guide branching heuristics of a Davis-Putnam Logemann-Loveland (DPLL) complete solver. Numerical experiments show that on random QBFs our branching heuristics gives robust exponential efficiency gain with respect to the state-of-art solvers. We also manage to solve some previously unsolved benchmarks from the QBFLIB library. Apart from this our study sheds light on using message passing in small systems and as subroutines in complete solvers. |
|
|
|
|