Solving QBF with Heuristic
Small-world Optimization Search Algorithm
1Modern Education and Technology Center, South China Agricultural University, China
2School of Computer Science and Engineering, South China University of Technology, China
Abstract: In this paper, we use Gaifman graph to describe the topological structure of the Quantified Boolean Formulae (QBF), we mainly study the formula family with the small-world network topology. We analyze the traditional Putnam, Logemann and Loveland (DPLL) solving algorithm for QBF, then we improve the DPLL algorithm and propose the solving algorithm framework based on small world optimization search algorithm, we apply this small world optimization search algorithm to determine the order of the DPLL branch variable. Our result proves that small world optimization search algorithm has a certain degree of effectiveness to improve the solving efficiency. It is valuable as an incomplete solution algorithm for search-based solver.
Keywords: QBF, small-world, search algorithm, optimization algorithm.
Received July 26, 2012; accepted February 11, 2013