SMT-Select: Multimodal Learning for SMT Algorithm Selection

SMT-Select is a unified framework for SMT algorithm selection that learns representations from both formula AST and natural-language contextual descriptions (such as the ones in SMT-LIB headers).

This repository accompanies the forthcoming CP 2026 paper “Learning Unified Graph and Language Representations for SMT Algorithm Selection.” It contains the implementation, processed data, trained models, and experiment outputs used to reproduce the paper's results.

We offer the following variants, tailored to different data-availability and computational-resource scenarios:

• SMT-Select (Graph + Text): the full multimodal version that uses GNN and pretrained sentence encoder to represent SMT instances.
• SMT-Select-Graph: GNN-based algorithm selector.
• SMT-Select-Text: SVM-based algorithm selector using descripton embeddings only.
• SMT-Lite: SVM-based algorithm selector using lightweight syntactic features.
• SMT-Lite+Text: SMT-Lite combined with textual embeddings.

Setup

Requires Python 3.10+.

python -m venv .venv && source .venv/bin/activate
pip install -e .

Reproducing the CP 2026 Results

Data Overview and Preparation

Raw performance data lives in data/raw_data/smtcomp24_performance/. Five random train-test splits per logic are in data/train_test_splits/ (create them with scripts/split_data_json.py and the desired seeds).

Download the corresponding SMT-LIB benchmarks before reproducing results. scripts/download_smtlib.sh downloads one logic at a time (pass the logic name as the only argument) under smtlib/. Example:

./scripts/download_smtlib.sh QF_BV

Our experimental results are stored in data/results. The reproduction instructions for each variant are provided below.

SMT-Select-Lite

Precomputed syntactic features for all logic benchmarks, plus extraction times from Klammerhammer, are in data/features/syntactic. After downloading the benchmarks, reproduce these tables for one logic with:

Build Klammerhammer from its linked source and place the executable at bin/klhm (the binary is not versioned in this repository). Alternatively, pass its location explicitly with --klhm /path/to/klhm.

python scripts/extract_syntactic_features.py --logic QF_BV

Omit --logic to process every available logic. Use --jobs to run multiple Klammerhammer processes concurrently. The script reads benchmark paths from data/raw_data/meta_info/, expects SMT-LIB files under smtlib/non-incremental/, and writes each logic's features.csv and extraction_times.csv under data/features/syntactic/.

To run SVM experiments over the five splits for a given logic (e.g. QF_BV):

python scripts/experiment_tabular.py --logic QF_BV --features-dir data/features/syntactic --output-dir data/results/lite

Results are saved to data/results/lite/<logic>/ (e.g. summary.json, and per-seed seed<N>/train_eval.csv, seed<N>/test_eval.csv).

SMT-Select-Text

Descriptions are saved in data/descriptions/. Encode descriptions to feature CSVs (by default using the all-mpnet-base-v2 model):

python scripts/encode_desc_logics.py --output-dir data/features/desc/all-mpnet-base-v2

Then run the experiments:

python scripts/experiment_tabular.py --logic QF_BV --features-dir data/features/desc/all-mpnet-base-v2 --output-dir data/results/text/all-mpnet-base-v2

Results go to data/results/text/all-mpnet-base-v2/<logic>/ (e.g. summary.json, per-seed CSVs). Use --model-name in encode_desc_logics for another encoder; omit --logic to run all logics that have desc features and splits.

SMT-Select-Lite+Text

SMT-Select-Lite+Text concatenates syntactic features with description embeddings from benchmark descriptions.

Run the experiments:

python scripts/experiment_tabular.py --logic QF_BV --features-dir data/features/syntactic data/features/desc/all-mpnet-base-v2 --output-dir data/results/lite+text/all-mpnet-base-v2

Results are saved to data/results/lite+text/all-mpnet-base-v2/<logic>/.

SMT-Select-Graph

To run experiments over the five splits for a given logic (e.g. ABV):

python scripts/experiment_graph.py --logic ABV

This automatically uses performance splits from data/train_test_splits/ABV/, SMT-LIB benchmarks under smtlib/non-incremental/, and writes results to data/results/graph/ABV/ (per-seed CSVs plus summary.json). Trained GIN models for each split are saved under models/gin_pwc/ABV/seed<N>/, and you can rerun only evaluation with --eval-only (reusing our saved models under models/gin_pwc/) to reproduce results without retraining.

For larger datasets, namely QF_BV, QF_LIA, QF_SLIA, and UFNIA, we enable a --filter flag that excludes training instances solved by all solvers within 24 seconds.

SMT-Select-Graph+Text

SMT-Select-Graph+Text trains multimodal solver-selection layers based on GIN-based graph embeddings and description embeddings.

We store precomputed GIN graph embeddings for each logic under data/features/graph/, and the description embeddings are the same as in SMT-Select-Text (e.g. data/features/desc/all-mpnet-base-v2/). To (re)compute GIN embeddings for a given logic (e.g. ABV) from your trained GIN models:

python scripts/extract_gin_embeddings.py ABV

This command looks for models under models/gin_pwc/ABV/seed*/, benchmarks in data/raw_data/smtcomp24_performance/ABV.json, and writes seed-wise graph features to data/features/graph/ABV/seed*/.

To run the multimodal fusion experiments over the five splits for a logic (e.g. ABV), using precomputed graph and text features:

python scripts/experiment_graph_text.py --logic ABV

This will load the corresponding graph and text feature directories, train the fusion model across all seeds, and write results to data/results/graph+text/all-mpnet-base-v2/ABV/ (per-seed train_eval.csv/test_eval.csv plus summary.json). Trained fusion models are saved under models/fusion_pwc/ABV/seed<N>/.

Our saved models live under models/fusion_pwc/, and you can also run evaluation only using the --eval-only flag.

Baselines

We evaluate MachSMT at e524a61 and Sibyl at 133d33f.

Citation

@inproceedings{smtselect_cp26,
  author    = {Lu, Zhengyang and Sarnighausen-Cahn, Paul and Chen, Jiahao and
               Gurfinkel, Arie and Manea, Florin and Ganesh, Vijay},
  title     = {Learning Unified Graph and Language Representations for {SMT}
               Algorithm Selection},
  booktitle = {The 32nd International Conference on Principles and Practice of
               Constraint Programming (CP 2026)},
  year      = {2026},
  note      = {To appear}
}