PALSAT: Deep Cooperation of Unit Propagation and Local Search in Incomplete SAT Solving

Towards Cardinality-Aware Local Search for SAT with Cardinality Constraints

SAT Solver Selection: Move Beyond Handcrafted Features

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.

Poster: Neural Network-Based SAT Solver Selection Using Instance 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.

Factoring Learned Clauses

This paper revisits previous work on ER, which factors out repeated parts of learned clauses during conflict analysis, and explores how their original strategy benefits from 15 years of improvements in the state-of-the-art solver CaDiCaL, and proposes a new, less intrusive inprocessing approach based on factoring XOR and ITE gates from learned clauses globally.

Towards Step-Wise Explanations of Large Search Trees (Short Paper)

From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming

This work presents the first systematic analysis of how leading LCG solvers maintain their SAT encodings, based on source-code inspection and developer correspondence, and proposes a native CDCL framework for CP, replacing SAT literals with atomic constraints, enabling conflict analysis, nogood learning, and nogood propagation directly at the CP level.