SMTS is a comprehensive divide-and-conquer distributed/parallel SMT solving framework where the input formula is partitioned into a tree structure in an iterative way. It also supports sharing of lemmas between solvers and allows a combination with portfolio solving. The tool is designed using a client-server architecture with TCP/IP communication, implemented in C++ and Python.
The framework is currently instantiated with OpenSMT as the underlying solver. The project is developed open-source and maintained at Github .
The theoretical aspects and underlying algorithms with parameters are described in [1]. The sections below add details on further optimizations and provide the full list of parameters with their default values.
Since 2021, SMTS consistently dominates in SMT-COMP parallel and cloud tracks in divisions that include the logics QF_UF, QF_LRA and QF_LIA. Refer to the following links at smt-comp.github.io for concrete results in the logics QF_LRA and QF_LIA:
- 2025/results/qf_lra-parallel , 2025/results/qf_lia-parallel
- 2024/results/qf_lra-cloud , 2024/results/qf_lia-cloud
- 2022/results/qf-lra-cloud , 2022/results/qf-lia-cloud
- 2021/results/qf-lra-cloud , 2021/results/qf-lia-cloud
Further Partitioning Optimizations
Expansion Boost Factor. In order to make the expansion avoidance more flexible, the partition tree expansion algorithm (Alg. 4, [1]) can further be parametrized by an expansion boost factor b ∈ [-1,1] by changing the expression 1/p in r ≥ 1/p (in line 8) to (1/p)(1 - b2) + (b/2)(1 + b):
- With b = 0, the parameter has no effect and the expression evaluates to 1/p.
- With b = -1, the expansion always aborts (at that point).
- With b = 1, the expansion never aborts (at that point).
The behavior also depends on the number of generated children p. If p = 2, the polynomial simplifies to a linear expression (1 + b)/2, but other values are viable too.
List of Parameters
The table below compiles the list of parameters for the partitioning algorithms (Section 3, [1]), sorted in alphabetical order.
The variables refer to the configuration variables used in server/config/default.py.
It also includes parameters that have only been mentioned within optimizations in Section 3 and in the “Further Partitioning Optimizations” section above.
| Name | Variable | Description | Default |
|---|---|---|---|
| b ∈ [-1,1] | partitioning_boost_factor | expansion boost factor | 0 |
| dynTSMult > 1 | dynamic_node_timeout_factor | multiplier of TS when TS is increased | 2 |
| dynTSThreshold ≥ 1 | dynamic_node_timeout_threshold_factor | threshold factor of TS when to increase TS | 4 |
| k ≥ 1 | max_tree_size_factor | maximum factor of the size of the tree | 2 |
| minPortfolio ≥ 1 | portfolio_min | minimum size of internal portfolios | 1 |
| nodeTSThreshold ≥ 1 | n_timeouts_to_count_partition | |tree| counts only nodes with node.time < ☆ . TS | 4 |
| p ≥ 2 | partition_policy | #created child nodes when partitioning | 2 |
| TS > 0 | node_timeout | solver timeout | 32 |
Published papers:
