Home | Contact | Sitemap | 中文 | CAS
Search: 
Home │  About Us │  Research │  People │  International Cooperation │  Education & Training │  Papers
  Seminar
Conference
Forum on FS
Colloquium
Seminar
Lunch Seminar
Coffee Time
Advanced Course
KITPC Activities
Other activities
  Location: Home >  Research Activities >  Seminar
Message passing for quantified Boolean formulas
2012-02-10     Text Size:  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.

  Appendix:
       Address: No. 55 Zhong Guan Cun East Road, Haidian District, Beijing 100190, P. R. China
Copyright ? Institute of Theoretical Physics, Chinese Academy of Sciences, All Rights Reserved