A Hybrid Learning Framework for Automated SAT Solver Selection

Abstract

Boolean Satisfiability (SAT) solving underlies a wide range of practical applications, including hardware verification, software testing, automated planning, and combinatorial design. Decades of engineering effort have produced highly optimised Conflict-Driven Clause Learning (CDCL) solvers, yet empirical studies consistently show that no single solver dominates across all problem instances; different solvers exhibit strongly complementary performance depending on the structural properties of the formula being solved. This observation motivates per-instance algorithm selection rather than reliance on a single fixed solver. Existing portfolio-based selectors, most notably SATzilla, rely on manually engineered structural and probing features that are informative but costly to compute and may not capture higher-order relational structure present in a formula's clause-variable graph. More recent graph neural network (GNN) approaches learn structural embeddings directly from the instance graph, but typically discard the substantial domain expertise encoded in handcrafted feature sets and can require considerable training data to generalise reliably to unseen instance families. This project proposes a hybrid learning framework that fuses handcrafted, SATzilla-style instance features with GNN-derived structural embeddings within a unified meta-classifier, combining the sample efficiency and interpretability of feature-based selection with the representational flexibility of graph learning. Each SAT instance will be represented as a literal-clause graph from which both a handcrafted feature vector and a learned graph embedding are extracted; at least two fusion strategies for combining the two representations will be implemented and compared. The framework will be trained and evaluated on benchmark instances drawn from recent SAT Competition benchmark suites, using a portfolio of established open-source CDCL solvers, and assessed against the single-best-solver baseline and the virtual-best-solver oracle using standard algorithm-selection metrics such as PAR10. It is anticipated that the hybrid approach will achieve higher selection accuracy and lower penalised average runtime than either a purely feature-based or a purely graph-based selector evaluated in isolation.