Aug 2026· Proceedings of the 32nd ACM SIGKDD Conference on Knowledge Discovery and Data Mining V.2· pp. 6618-6628· 0 citations· 10 references
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.
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.
Takeru Nagahama, Tomohisa Kawakami, Tomoyasu Shimada et al.· IEEE International Conferenc...· 0 citations
Evaluated across nine SMT logics, SMT-Select consistently outperforms existing selectors and SMT-COMP winning solvers and closes at least 30% of the performance gap between the competition winner and the virtual best solver (VBS).
Zhengyang Lu, Paul Sarnighausen-Cahn, Jiahao Chen et al.· International Conference on...· 0 citations
An automated approach that uses Large Language Models in an agentic check--fix--verify loop to synthesize executable Python scripts that act as interpretable, problem-specific feature extractors that consistently outperform both expert-curated mzn2feat features and the best transformer-based trans2feat variants.
Hai Xia, C. Ansótegui, Stefan Szeider· 0 citations
The PALSAT (Progressive Activation Local Search for SAT) incomplete solver is proposed, which integrates the core techniques from both sides, Unit Propagation (UP) and LS, and leads to some promising results.
Mingming Jin, Zhijie Kuang, Jiongzhi Zheng et al.· International Conference on...· 0 citations
An automatic pipeline that is problem-agnostic to all problems in the MiniZinc format is built, finding that algorithm selection achieves a 39.6% average problem-weighted win rate against a one-shot Gurobi baseline, more than doubling the best single configuration (19.3%).
Hai Xia, Vaidyanathan Peruvemba Ramaswamy, Stefan Szeider· 0 citations
