A Concurrent Portfolio Approach to SMT Solving Export

@incollection{citeulike:6083578, abstract = {With the availability of multi-core processors and large-scale computing clusters, the study of parallel algorithms has been revived throughout the industry. We present a portfolio approach to deciding the satisfiability of SMT formulas, based on the recent success of related algorithms for the SAT problem. Our parallel version of Z3 outperforms the sequential solver, with speedups of well over an order of magnitude on many benchmarks.}, author = {Wintersteiger, Christoph and Hamadi, Youssef and de Moura, Leonardo}, citeulike-article-id = {6083578}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-02658-4_60}, citeulike-linkout-1 = {http://www.springerlink.com/content/103u1346q4666256}, doi = {10.1007/978-3-642-02658-4_60}, journal = {Computer Aided Verification}, keywords = {cav, parallel, sat, smt}, pages = {715--720}, posted-at = {2009-11-08 01:05:07}, priority = {2}, title = {A Concurrent Portfolio Approach to SMT Solving}, url = {http://dx.doi.org/10.1007/978-3-642-02658-4_60}, year = {2009} }

TY - CHAP ID - citeulike:6083578 L3 - citeulike-article-id:6083578 N2 - With the availability of multi-core processors and large-scale computing clusters, the study of parallel algorithms has been revived throughout the industry. We present a portfolio approach to deciding the satisfiability of SMT formulas, based on the recent success of related algorithms for the SAT problem. Our parallel version of Z3 outperforms the sequential solver, with speedups of well over an order of magnitude on many benchmarks. JF - Computer Aided Verification EP - 720 TI - A Concurrent Portfolio Approach to SMT Solving SP - 715 KW - cav KW - parallel KW - sat KW - smt AU - Wintersteiger, Christoph AU - Hamadi, Youssef AU - de Moura, Leonardo PY - 2009/// UR - http://dx.doi.org/10.1007/978-3-642-02658-4_60 ER -