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.

We build the first machine-learning-based algorithm selection tool for hardware verification described in the Btor2 format. In addition to hardware verifiers, our tool also selects from a set of software verifiers to solve a given Btor2 instance, enabled by a Btor2-to-C translator. We propose two embeddings for a Btor2 instance, Bag of Keywords and Bit-Width Aggregation. Pairwise classifiers are applied for algorithm selection. Upon evaluation, our tool Btor2-Select solves 30.0% more instances and reduces PAR-2 by 50.2%, compared to the PDR implementation in the HWMCC'20 winner model checker AVR. Measured by the Shapley values, the software verifiers collectively contributed 27.2% to Btor2-Select's performance.

Abstract In recent years, a diverse variety of hardware model-checking tools and techniques that exhibit complementary strengths and distinct weaknesses have been proposed. This state of affairs naturally suggests the use of algorithm-selection techniques to select the right tool for a given instance. To automate this process, we present Btor2-Select , a machine learning-based algorithm-selection framework for the hardware model-checking problem described in the word-level modeling language Btor2 . The framework offers an efficient and effective machine-learning pipeline for training an algorithm selector. Btor2-Select also enables the use of the trained selector to predict the most suitable off-the-shelf model checker for a given verification task and automatically invoke it to solve the task. Evaluated on a comprehensive Btor2 benchmark suite coupled with a set of state-of-the-art model checkers, Btor2-Select trained an algorithm selector that successfully closed over 65 % of the PAR-2 performance gap between the best single tool and the idealized virtual selector. Moreover, the selector outperformed a portfolio model checker that runs three complementary verification engines in parallel. Btor2-Select offers a simple, systematic, and extensible solution to harness the complementary strengths of diverse model checkers. With its fast and highly configurable training procedure, Btor2-Select can be easily integrated with new tools and applied to various application domains.

Abstract Modern SMT solvers, such as Z3, allow solver users to customize strategies to improve performance on their specific use cases. However, handcrafting an optimized strategy for a specific class of SMT instances remains a complex and demanding task for both solver developers and users alike. In this paper, we address the problem of automated SMT strategy synthesis via a novel method based on Monte-Carlo Tree Search (MCTS). We formulate strategy synthesis as a sequential decision-making process, where the search tree corresponds to the strategy space. Subsequently, we employ MCTS to navigate this vast search space. Compared to the conventional MCTS, we introduce two heuristics—layered and staged search—that enable our method to identify effective strategies with lower costs. We implement our method, dubbed Z3alpha, upon the Z3 SMT solver. Our experiments demonstrate that Z3alpha outperforms the default Z3 solver and the state-of-the-art synthesis tool Fastsmt on the majority of the evaluated benchmark sets, while producing more interpretable strategies than FastSMT. At SMT-COMP’24, among the 16 participating logics, Z3alpha improved upon the default Z3 in 12 cases and helped solve hundreds more instances in QF_NIA and QF_NRA, winning their respective divisions.