Parallel Optimization Technology For Satisfiability Problem Based On Multi-core Platform

As a fundamental theoretical issue in the field of software vulnerability mining,the Satisfiability Problem is of great significance to detecting software vulnerabilities and ensuring software security.Nowadays,the complicated software environment in modern society has put forward higher requirements on the speed of solving the satisfiability problem.In this paper,we studies the parallel optimization techniques for satisfiability based on the high-performance multi-core ARM platform.For the Boolector solver of SMT,we use the method of coarse-grained parallelism to improve the throughput of the solver by taking advantage of the single-core computing ability and more cores of the ARM platform.We also adopt the static scheduling,dynamic scheduling,as well as our proposed dynamic scheduling strategy based on time order,to schedule data.Ultimately,we get a better speedup ratio on ARM platform,which is 3.63 times superior to that on the mainstream X86 platform.For the Minisat solver of SAT,we use both of the coarse-grained and fine-grained parallel techniques simultaneously.The coarse-grained parallelism is mainly used to improve the throughput while the fine grained parallization is mainly used to shorten the long-tail effect and balance the thread load.In addition,we use the time prediction model to predict the approximate running time of the solution instance so that the input data set can be sorted according to the running time,so as to give full play to the optimization effect of the dynamic scheduling strategy based on time order.In the test,we get a 3.46 times better performance on ARM platform than that on the mainstream X86 platform.