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 (SW) network topology. We analyze the t raditional Davis, Putnam, Logemann and Loveland (DPLL) solving algori thm for QBF, then we improve the DPLL algorithm and propose the solving algorithm framework based on Small World Op timization Search (SWOS) algorithm, we apply this SWOS algorithm to determine the order of the DPLL branch variable. Ou r result proves that SWOS algorithm has a certain degree of effectiveness to improve the solving efficiency. It is valuable a s an incomplete solution algorithm for search1based solver.

References

[1] Baader F. and Voronkov A., Evaluating QBFs via Symbolic Skolemization, in Proceedings of Logic for Programming, Artificial Intelligence and Reasoning , Montevideo, Uruguay, pp. 2852 300, 2005.

[2] Balabanov V. and Jiang J., Unified QBF Certification and its Applications, Formal Methods in System Design , vol. 41, no. 1, pp. 452 65, 2012.

[3] Benedetti M., sKizzo: A Suite to Evaluate and Certify QBFs, in Proceedings of the 20 th International Conference on Automated Deduction , Tallinn, Estonia, pp. 3692376, 2005.

[4] Biere A., Resolve and Expand, in Proceedings of the 7 th International Conference on Theory and Applications of Satisfiability Testing , BC, Canada, pp. 59270, 2005.

[5] Bodlaender H., Treewidth: Characterizations, Applications and Computations, in Proceedings of the 32 nd International Workshop of Graph1 Theoretic Concepts in Computer Science , Bergen, Norway, pp. 1214, 2006.

[6] Cadoli M., Schaerf M., Giovanardi A., and Giovanardi M., An Algorithm to Evaluate Quantified Boolean Formulae and its Experimental Evaluation, the Journal of Automated Reasoning , vol. 28, no. 2, pp. 1012142, 2002.

[7] Dershowitz N., Hanna Z., and Katz J., Bounded Model Checking With QBF, in Proceedings of the 8 th International Conference on Theory and Applications of Satisfiability Testing , St Andrews, UK, pp. 4082414, 2005.

[8] Feldmann R., Monien B., and Schamberger S., A Distributed Algorithm to Evaluate Quantified Boolean Formulae, in Proceedings of AAAI100 , Texas, USA, pp. 126, 2000.

[9] Gent I., Hoos H., Rowley A., and Smyth K., Using Stochastic Local Search To Solve Quantified Boolean Formulae, in Proceedings of the 9 th International Conference on Principles and Practice of Constraint Programming , Kinsale, Ireland, pp. 3482362, 2003.

[10] Giunchiglia E., Narizzano M., and Tacchella A., Clause/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas, the Journal of Artificial Intelligence Research , vol. 26, no. 2, pp. 3712416, 2006.

[11] Giunchiglia E., Narizzano M., and Tacchella A., QuBE++: An Efficient QBF Solver, in Proceedings of the 5 th International Conference on Formal Methods in Computer1Aided Design , Texas, USA, pp. 2012213, 2004.

[12] Janota M., Klieber W., Marques2Silva J., and Clarke E., Solving QBF with Counterexample Guided Refinement, in Proceedings of the 15 th International Conference on Theory and Applications of Satisfiability Testing , Trento, Italy, pp. 1142128, 2012.

[13] Jussila T. and Biere A., Compressing BMC Encodings with QBF, Electronic Notes in Theoretical Computer Science , vol. 174, no. 3, pp. 45256, 2007.

[14] Kullmann O., Theory and Applications of Satisfiability Testing, in Proceedings of the 12 th International Conference on Theory and Applications of Satisfiability Testing , Swansea, UK, pp. 4302435, 2009.

[15] Lewis M., Schubert T., Becker B., Marin P., Narizzano M., and Giunchiglia E., Parallel QBF Solving with Advanced Knowledge Sharing, Fundamenta Informaticae , vol. 107, no. 2, pp. 1392166, 2011.

[16] Lewis M., Schubert T., and Becker B., QMiraXT1A Multithreaded QBF Solver , Univerlagtuberlin Press, Berlin, 2009.

[17] Marin P., Miller C., and Becker B., Incremental QBF Preprocessing For Partial Design Verification, in Proceedings of the 15 th International Conference on Theory and Applications of Satisfiability Testing , Trento, Italy, pp. 4732474, 2012.

[18] Peschiera C., Pulina L., Tacchella A., Bubeck U., Kullmann O., and Lynce I., The 7th QBF Solvers Evaluation (QBFEVAL 10), in Proceedings of the 13 th International Conference on Theory and Applications of Satisfiability Testing , Edinburgh, UK, pp. 2372250, 2010.

[19] Pigorsch F. and Scholl C., Exploiting Structure in an AIG Based QBF Solver, in Proceedings of Conference on Design , Automation and Test in Europe , Nice, France, pp. 159621601, 2009.

[20] Pulina L. and Tacchella A., A Self2adaptive Multi2engine Solver for Quantified Boolean 378 The International Arab Journal of Informatio n Technology, Vol. 12, No. 4, July 2015 Formulas, Constraints, vol. 14, no. 1, pp. 802116, 2009.

[21] Pulina L. and Tacchella A., A Structural Approach to Reasoning with Quantified Boolean Formulas, in Proceedings of the 21 st International Joint Conference on Artificial Intelligence , Italy, pp.5962602, 2009.

[22] Pulina L. and Tacchella A., An Empirical Study of QBF Encodings: From Treewidth Estimation to Useful Preprocessing, Fundamenta Informaticae , vol. 102, no. 3, pp.3912427, 2010.

[23] Pulina L. and Tacchella A., Hard QBF Encodings Made Easy: Dream or Reality?, in Proceedings of the 11 th International Conference of the Italian Association for Artificial Intelligence , Reggio Emilia, Italy, pp. 31234, 2009.

[24] Sadeghi M., Maghooli K., and Moein M., Using Artificial Immunity Network for Face Verification, the International Arab Journal of Information Technology , vol. 11, no. 4, pp.1002 106, 2014.

[25] Samulowitz H. and Memisevic R., Learning to solve QBF, in Proceedings of the 22 nd Conference on Artificial Intelligence , Canada, pp. 2552260, 2007.

[26] Walsh T., Search in a Small World, in Proceedings of the 16 th International Joint Conference on Artificial Intelligence , CA, USA, pp. 117221177, 1999.

[27] Watts D. and Strogatz S., Collective Dynamics of Small2World Networks, Nature, vol. 393, no. 6684, pp. 4402442, 1998.

[28] Yan X., Zhao J., and Shi H., Network2Structure Group Search Optimization Algorithm Based on an Improved Small World Topology and it Application, Computers and Applied Chemistry , vol. 28, no. 7, pp. 9232927, 2011.

[29] Yin M., Zhou J., Sun J., and Gu W., Heuristic Survey Propagation Algorithm for Solving QBF Problem, Ruanjian Xuebao/Journal of Software , vol. 22, no. 7, pp. 153821550, 2011. Tao Li is a scientific researcher and project manager in Modern Education and Technology Center, South China Agricultural University and holds an IEEE membership. He completed his PhD degree in School of Computer Science and Engineering, South China University of Technology. His research interests include intelligent computin g and data mining. Nanfeng Xiao is currently a Professor and PhD tutor of computer science in School of Computer Science and Engineering, South China University of Technology. His research interests are in the areas of intelligent computing, intelligent robots and data mining.