Parallel solving model for quantified boolean formula based on machine learning

Abstract

A new parallel architecture for quantified boolean formula (QBF) solving was proposed, and the prediction model based on machine learning technology was proposed for how sharing knowledge affects the solving performance in QBF parallel solving system, and the experimental evaluation scheme was also designed. It shows that the characterization factor of clause and cube influence the solving performance markedly in our experiment. At the same time, the heuristic machine learning algorithm was applied, support vector machine was chosen to predict the performance of QBF parallel solving system based on clause sharing and cube sharing. The relative error of accuracy for prediction can be controlled in a reasonable range of 20%–30%. The results show the important and complex role that knowledge sharing plays in any modern parallel solver. It shows that the parallel solver with machine learning reduces the quantity of knowledge sharing about 30% and saving computational resource but does not reduce the performance of solving system.

Keywords

machine learning / quantified boolean formula / parallel solving / knowledge sharing / feature extraction / performance prediction

References

[1] LewisM, MarinP, SchubertT, NarizzanoM, BeckerB, GiunchigliaE. PaQuBE: Distributed QBF solving with advanced knowledge sharing [J]. Lecture Notes in Computer Science, 2009, 5584: 509-523

[2] MotaB D, NicolasP, StephanI. A new parallel architecture for QBF tools [C]. Proceeding of 2010 International Conference on High Performance Computing and Simulation, 2010PerthIEEE Press324-330

[3] LewisM, SchubertT, BeckerB. Parallel QBF solving with advanced knowledge sharing [J]. Fundamenta Informaticae, 2011, 107(3): 139-166

[4] CadoliM, SchaerfM, GiovanardiA, GiovanardiM. An algorithm to evaluate quantified boolean formulae and its experimental evaluation [J]. Journal of Automated Reasoning, 2002, 28(2): 101-142

[5] LewisM, SchubertT, BeckerB. QMiraXT-a multithreaded QBF solver. Methoden und beschreibungssprachen zur modellierung und verifikation von schaltungen und systemen [M], 2009BerlinUniverlagtuberlin

[6] GiunchigliaE, NarizzanoM, TacchellaA. QuBE++: An efficient QBF solver [J]. Lecture Notes in Computer Science, 2004, 3312: 201-213

[7] GiunchigliaE, NarizzanoM, TacchellaA. Clause/term resolution and learning in the evaluation of quantified boolean formulas [J]. Journal of Artificial Intelligence Research, 2006, 26(8): 371-416

[8] YuY, MalikS. Validating the result of a quantified boolean formula (qbf) solver: Theory and practice [C]. Proceedings of the 2005 Asia and South Pacific Design Automation Conference, 2005New YorkACM Press1047-1051

[9] BiereA. Resolve and expand [J]. Lecture Notes in Computer Science, 2005, 3542: 59-70

[10] LonsingF, BiereA. Nenofex: Expanding NNF for QBF solving [J]. Lecture Notes in Computer Science, 2008, 4996: 196-210

[11] BenedettiM. sKizzo: A suite to evaluate and certify QBFs [J]. Lecture Notes in Computer Science, 2005, 3632: 369-376

[12] BaaderF, VoronkovA. Evaluating QBFs via symbolic skolemization [J]. Lecture Notes in Computer Science, 2005, 3452: 285-300

[13] PulinaL, TacchellaA. A self-adaptive multi-engine solver for quantified boolean formulas [J]. Constraints, 2009, 14(1): 80-116

[14] PigorschF, SchollC. Exploiting structure in an AIG based QBF solver [C]. Proceedings of the 2009 Conference on Design, Automation and Test in Europe, 2005New YorkACM Press01-06

[15] PanB, GuoH-xia. Parallel forward reasoning for mechanical proving of geometry theorem [J]. Journal of South China University of Technology (Natural Science Edition), 2008, 36(4): 93-97

[16] PiY-j, WangX-y, GuXi. Synchronous tracking control of 6-DOF hydraulic parallel manipulator using cascade control method [J]. Journal of Central South University of Technology, 2011, 18(5): 1554-1562

[17] YangC-f, ZhengS-t, JinJun. Forward kinematics analysis of parallel manipulator using modified global newton-raphson method [J]. Journal Of Central South University of Technology, 2010, 17(6): 1264-1270

[18] LiuS-z, YuY-q, ZhuZ-cai. Dynamic modeling and analysis of 3-RRS parallel manipulator with flexible links [J]. Journal of Central South University of Technology, 2010, 17(2): 323-331

[19] BlessieE C, KarthikeyanE. Sigmis: A feature selection algorithm using correlation based method [J]. Journal of Algorithms & Computational Technology, 2012, 6(3): 385-394

[20] LiuQ, LiuZ, HuangMin. Study on internet traffic classification using machine learning [J]. Computer Science, 2010, 37(12): 35-40

[21] ZhaoT-z, DongS-b, MarchV, SeeS. Predicting the parallel file system performance via machine learning [J]. Journal of Computer Research and Development, 2011, 48(7): 1202-1215

[22] CristianiniN, TaylorJ SAn introduction to support vector machines [M], 2000CambridgeCambridge University Press

[23] GuyonI, ElisseeffA. An introduction to variable and feature selection [J]. The Journal of Machine Learning Research, 2003, 3(3): 1157-1182

[24] NicholasT K, BrianT, IanF. MPICH-G2: A grid-enabled implementation of the message passing interface [J]. Journal of Parallel and Distributed Computing, 2003, 63(5): 551-563

[25] PlaistedD A, BiereA, ZhuY-shan. A satisfiability procedure for quantified boolean formulae [J]. Discrete Applied Mathematics, 2003, 130(2): 291-328