Graph neural network based time estimator for SAT solver

SAT-based formal verification is a systematic process to prove the correctness of computer hardware design based on formal specifications, providing an alternative to time-consuming simulations and ensuring design reliability and accuracy. Predicting the runtime of SAT solvers is important to effectively allocate verification resources and determine if the verification can be completed within time limits. Predicting SAT solver runtime is challenging due to variations in solving time across different solvers and dependence on problem complexity and solver mechanisms. Existing approaches rely on feature engineering and machine learning, but they have drawbacks in terms of expert knowledge requirements and time-consuming feature extraction. To address this, using graph neural networks (GNNs) for runtime prediction is considered, as they excel in capturing graph topology and relationships. However, directly applying existing GNNs to predict SAT solver runtime does not yield satisfactory results, as SAT solvers' proving procedure is crucial. In this paper, we propose a novel model, TESS, that integrates the working mechanism of SAT solvers with graph neural networks (GNNs) for predicting solving time. The model incorporates a graph representation inspired by the CDCL paradigm, proposes adaptive aggregation for multilayer information and separate modules for conflict learning. Experimental results on multiple datasets validate the effectiveness, scalability, and robustness of our model, outperforming baselines in SAT solver runtime prediction.