Poster: A Comparative Analysis of Machine Learning Models for SAT Runtime Prediction

The satisfiability (SAT) problem is one of the most fundamental NP-complete problems, and competitions for SAT solvers are held annually to benchmark solver performance. Accurate real-time prediction of solver runtime has become more important for optimal solver selection and efficient resource allocation, especially as solvers and hardware advance. In this work, we evaluate the performance of major machine learning models on SAT runtime prediction tasks, using recent SAT competition datasets. Furthermore, we use not only conventional evaluation metrics e.g., Root Mean Squared Error (RMSE) and Mean Absolute Error (MAE), but also more detailed metrics e.g., classification-based confusion matrices and cumulative error distributions. Consequently, we observe that the performance of random forest models, often showing the highest performance in previous studies, is poor and biased toward the median runtime, while the performance of Multilayer Perceptron (MLP) models is more robust even when their RMSE and MAE are higher. These results offer new insights not only for developing more reliable runtime prediction models but also for improving algorithm selection and resource management methods in SAT solving.