Advertisement
Published in:
2018 | OriginalPaper | Chapter
Parallel Satisfiability Modulo Theories
Authors : Antti E. J. Hyvärinen, Christoph M. Wintersteiger
Published in: Handbook of Parallel Constraint Reasoning
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Satisfiability Modulo Theories (SMT) is an extension of the propositional satisfiability problem (SAT) to other, well-chosen (first-order) theories such as integers, reals, and bit-vectors. This approach currently enjoys much popularity, especially in the field of software verification, where SMT solvers have become the de facto standard tool for the discharge of verification conditions. The development of parallel SMT solvers is still in its infancy, but the first general paradigms have been established. This chapter provides an overview of the recent advances in this area, specifically algorithm portfolio, search-space partitioning, and problem decomposition techniques, and how they relate to each other in theory and practice.