Poster: Neural Network-Based SAT Solver Selection Using Instance Features

Abstract

The Boolean satisfiability (SAT) problem is fundamental in applications such as verification and scheduling, where fast solving is often required. However, the performance of SAT solvers varies significantly across instances, making solver selection an important challenge. Previous studies have commonly employed random forest (RF)-based approaches, which have shown promising performance for SAT solver selection. However, these methods may struggle to capture complex higher-order feature interactions and do not directly optimize runtime, which is the primary objective in practice. To address these issues, we propose a solver selection method that combines a neural network with a custom loss function for runtime-aware training. Experiments on the SAT Competition 2024 dataset show that the proposed method reduces total runtime by 8.8% and improves selection accuracy by 3.2% compared with an RF-based baseline. These results suggest that neural-network-based models, combined with task-specific training objectives, provide a promising direction for SAT solver selection. The proposed framework may also be applicable to other computational problems, such as planning and scheduling.