SAT Solver Selection: Move Beyond Handcrafted Features
TL;DR
This work proposes an end-to-end approach for handcrafted Feature-Free SAT Solver Selection, called F2S3, which effectively captures the structural complexity of graph data, eliminates the need for handcrafted features, and improves feature representation in the low-dimensional space.
Abstract
Boolean Satisfiability (SAT) Problem is a cornerstone in computer science and artificial intelligence, underpinning numerous applications. Since no single SAT solver dominates all problem instances, SAT Solver Selection (SSS) leverages machine learning to dynamically choose the most effective algorithm. However, traditional SSS methods rely on handcrafted features, which are computationally expensive and require extensive domain expertise. To address this challenge, we propose an end-to-end approach for handcrafted Feature-Free SAT Solver Selection, called F2S3. This approach transforms problem instances into graph data, employing the Correlation Refinement Factor Graph to maintain higher-order structural properties and node relationships. The Dual-Proximity Graph Representation is then utilized to enhance the graph features and project them into low-dimensional vectors. Finally, the Sensitive-Associative Cascade Forest is applied to select the optimal SAT solver through classification. This method effectively captures the structural complexity of graph data, eliminates the need for handcrafted features, and improves feature representation in the low-dimensional space. Experiments conducted on the ASlib database dataset demonstrate that this method consistently outperforms state-of-the-art SSS approaches, achieving higher gap values while requiring less computation time compared to other manually computed features.