Abstract
This paper demonstrates the benefits of GPU parallelism for a simplex-based decision procedure for conjunctions of linear constraints over reals. This variant of the simplex method, called general simplex, decides whether the set of constraints is satisfiable, and is intended to be integrated into SMT solvers. We carried out comprehensive experiments over randomly generated instances for dense linear programming problems on a mid-range consumer GPU (AMD Radeon 390X) using floating point arithmetic. The GPU scheduled hundreds of thousands of concurrent thread workgroups to process tableaus representing up to 8k variables and 8k constraints. We achieved speedup up to 25x over a CPU-only implementation (quad-core AMD Kaveri 3.7 GHz) of the same procedure. We compared this to a multithreaded OpenMP implementation that also achieved up to 1.8x speedup on the same inputs. These results suggest that GPU processors may be further utilized in the context of SMT and software verification tools.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
- 4.
As described in [10], arbitrary weak linear constraints of the form \(L \otimes R\), where \(\otimes \in \{\le , \ge , = \}\), can be translated to general form as follows for the ith constraint: (1) move all addends in R to the left-hand side to obtain \(L' \otimes b\), where b is a constant; (2) introduce a new variable \(s_i\) and add the constraints \(L' - s_i = 0\) and \(s_i \otimes b\). The variables s are called additional variables.
- 5.
Note that we are using \(x_i\) here to refer to any variable, whether it be a decision or an additional variable.
References
Asanovic, K., Bodik, R., Catanzaro, B.C., Gebis, J.J., Husbands, P., Keutzer, K., Patterson, D.A., Plishker, W.L., Shalf, J., Williams, S.W., Yelick, K.A.: The landscape of parallel computing research: a view from Berkeley. Technical report UCB/EECS-2006-183, Berkeley EECS, December 2006
Beckers, S., De Samblanx, G., De Smedt, F., Goedeme, T., Struyf, L., Vennekens, J.: Parallel hybrid SAT solving using OpenCL (2012)
Borkar, S., Chien, A.A.: The future of microprocessors. CACM 54(5), 67–77 (2011). http://doi.acm.org/10.1145/1941487.1941507
Dantzig, G.B.: Linear Programming and Ext. Princeton University Press, Princeton (1963)
Deleau, H., Jaillet, C., Krajecki, M.: GPU4SAT: solving the SAT problem on GPU. In: PARA Workshop on Scientific & Parallel Computing (2008)
Dutertre, B., Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Faure, G., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: SAT modulo the theory of linear arithmetic: exact, inexact and commercial solvers. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 77–90. Springer, Heidelberg (2008)
Fujii, H., Fujimoto, N.: GPU Acceleration of BCP Procedure for SAT Algorithms (2012)
Gulati, K., Khatri, S.P.: Boolean satisfiability on a graphics processor, pp. 123–126 (2010)
Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer (2008)
Lalami, M.E., Boyer, V., El-Baz, D.: Efficient implementation of the simplex method on a CPU-GPU system. In: IEEE International Symposium on Parallel and Distributed Processing Workshops and Ph.D. Forum, pp. 1999–2006 (2011)
Lalami, M.E., El-Baz, D., Boyer, V.: Multi GPU implementation of the simplex algorithm. In: 2011 IEEE International Conference on High Performance Computing and Communications, Banff, Canada, pp. 179–186, September 2011
Meyer, Q., Schonfeld, F., Stamminger, M., Wanka, R.: 3-SAT on CUDA: towards a massively parallel SAT solver. In: High Performance Computing and Simulation (HPCS), pp. 306–313. IEEE (2010)
Mittal, S., Vetter, J.: A Survey of CPU-GPU Heterogeneous Computing Techniques. ACM Comput. Surv. 47, 1–35 (2015)
Monniaux, D.: On using floating-point computations to help an exact linear arithmetic decision procedure. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 570–583. Springer, Heidelberg (2009)
Munshi, A., Benedict, R.G., Mattson, T.G., Fung, J., Ginsburg, D.: OpenCL Programming Guide. Addison-Wesley, Reading (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Stewart, S.T., Rayside, D., Ganesh, V., Czarnecki, K. (2016). Accelerating the General Simplex Procedure for Linear Real Arithmetic via GPUs. In: Blazy, S., Chechik, M. (eds) Verified Software. Theories, Tools, and Experiments. VSTTE 2016. Lecture Notes in Computer Science(), vol 9971. Springer, Cham. https://doi.org/10.1007/978-3-319-48869-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-48869-1_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-48868-4
Online ISBN: 978-3-319-48869-1
eBook Packages: Computer ScienceComputer Science (R0)