Parallel SMT Solving via Dynamic Partitioning, Core-Guided Pruning, and Backbone Detection

Ilana Shapiro, Sorin Lerner, Nikolaj Bjørner

Exploiting parallelism in modern CPU architectures remains a longstanding challenge in optimizing SMT solvers. We introduce a novel framework for parallel SMT solving that uses fee…