DROPS

Document

DOI: 10.4230/LIPIcs.CP.2026.41

Learning Unified Graph and Language Representations for SMT Algorithm Selection

Authors: Zhengyang Lu, Paul Sarnighausen-Cahn, Jiahao Chen, Arie Gurfinkel, Florin Manea, and Vijay Ganesh

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract

Algorithm selection is important in satisfiability and constraint solving, since no single solver performs best across all instances. Traditional learning-based approaches represent problem instances using expert-designed features to predict solver performance, while recent work explores graph representations derived from ASTs. However, most existing approaches overlook high-level contextual information, such as the application domain or the benchmark origin. In practice, such cues often help practitioners choose an appropriate solver. We present SMT-Select, a multimodal framework for SMT algorithm selection. It learns graph representations from formula ASTs and textual representations from natural-language context descriptions. These representations are then combined to guide solver selection. Evaluated across nine SMT logics, SMT-Select consistently outperforms existing selectors and SMT-COMP winning solvers. Across all evaluated logics, it closes at least 30% of the performance gap between the competition winner and the virtual best solver (VBS), and nearly matches the VBS in two logics.

Cite as

Zhengyang Lu, Paul Sarnighausen-Cahn, Jiahao Chen, Arie Gurfinkel, Florin Manea, and Vijay Ganesh. Learning Unified Graph and Language Representations for SMT Algorithm Selection. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 41:1-41:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{lu_et_al:LIPIcs.CP.2026.41,
  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 =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{41:1--41:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.41},
  URN =		{urn:nbn:de:0030-drops-266736},
  doi =		{10.4230/LIPIcs.CP.2026.41},
  annote =	{Keywords: satisfiability modulo theories, algorithm selection, multimodal learning, neuro-symbolic AI}
}

Search Results

Documents authored by Lu, Zhengyang

Learning Unified Graph and Language Representations for SMT Algorithm Selection

Abstract

Cite as

Thanks for your feedback!

Could not send message