Home // FUTURE COMPUTING 2014, The Sixth International Conference on Future Computational Technologies and Applications // View article

An Improvement on Acceleration of Distributed SMT Solving

Authors:
Leyuan Liu
Weiqiang Kong
Takahiro Ando
Hirokazu Yatsu
Akira Fukuda

Keywords: Satisfiability Modulo Theories; Distributed Solving; Acceleration; MPI; OpenMP.

Abstract:
Satisfiability Modulo Theories-based Bounded Model Checking consists of two primary tasks: (1) encoding a bounded model checking problem into a propositional formula that represents the problem, and (2) using a SMT solver to solve the formula. Solving the formula (namely, SMT solving) involves computation-intensive processes and is thus time-consuming. The target of this paper is to improve the distributed SMT solving techniques we previously proposed for further enhancing the effectiveness of SMT-based BMC. To this end, we improve the file dispatching scheme and reform the communication protocols in our previous work. In this paper, we describe the amelioration details and give a series of experiments to show the effectiveness of our improvement. Experimental results show that the improved implementation outperform the previous one. In addition to solving 8 groups of benchmarks by increasing the number of clients, we also make a preliminary experiment on increasing Central Processing Unit cores to investigate the influence.

Pages: 69 to 75

Copyright: Copyright (c) IARIA, 2014

Publication date: May 25, 2014

Published in: conference

ISSN: 2308-3735

ISBN: 978-1-61208-339-1

Location: Venice, Italy

Dates: from May 25, 2014 to May 29, 2014