We present a novel algorithm for parallel solving of SMT problems based on a partitioning process that divides the original problem into a tree structure in an iterative way. By enabling node revisiting, the new method addresses the problem of partitioning divergence found in prior approaches that frequently leads to longer runtimes compared to sequential results. The resulting algorithm is highly flexible, offers a combination of partitioning, portfolio solving, and clause sharing, allows the use of various partitioning functions, and scales gracefully with the available resources. We implemented the new approach in the tool SMTS on top of the efficient sequential SMT solver OpenSMT. Our experimental results demonstrate a substantial improvement over OpenSMT in logics QF_LRA and QF_LIA even when the partitioning approach utilizes just a single solver. Notably, SMTS has consistently dominated several divisions of the annual competition of parallel SMT solvers.
Metric Interval Temporal Logic ( ) is a popular formalism for specifying properties of reactive systems with timing constraints. Existing approaches to using in verification tasks, however, have notable drawbacks: they either support only limited fragments of the logic (the future only fragment [] ) or allow for only incomplete verification. This paper introduces MightyPPL , a new tool for translating formulae in Metric Interval Temporal Logic with Past and Pnueli modalities ( ) over the pointwise semantics into timed automata, enabling satisfiability and model checking of this expressive specification logic over both finite and infinite timed words. MightyPPL optimises performance via specialised constructions for simple cases, a novel symbolic transition encoding, and a symmetry reduction technique that yields an exponential improvement in reachable discrete states. The tool generates language-equivalent automata compatible with back-ends such as Uppaal, TChecker, and LTSmin. Our evaluation demonstrates that MightyPPL significantly outperforms the state-of-the-art tool MightyL on future-only fragments and across various benchmarks.
