Towards Cardinality-Aware Local Search for SAT with Cardinality Constraints
Towards Cardinality-Aware Local Search for SAT with Cardinality Constraints
Shuli Hu, Dian Ling, Jiaqi Li, Minghao Yin
Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence
Main Track. Pages 2256-2264.
https://doi.org/10.24963/ijcai.2026/251
Satisfiability (SAT) with cardinality constraints arises naturally in many practical applications, where high-level counting requirements coexist with standard Conjunctive Normal Form (CNF) clauses. Translating these constraints into CNF can destroy structural information, limiting the effectiveness of search-based heuristics. In this paper, we propose a cardinality-aware local search framework to solve this problem, denoted as CardSAT-LS. CardSAT-LS integrates a preprocessing phase based on the generalized unit propagation and resolution, a cardinality-sensitive scoring function combining the make-break mechanism and cardinality violation, and an initialization based on fake-backbone variables. Furthermore, CardSAT-LS employs a unified framework that adaptively alternates between flip and swap operators when the search gets trapped in local optima. Finally, we conduct experiments on five public benchmarks from real-world applications as well as the MaxSAT and SAT competitions. Compared with ten state-of-the-art competitors, including SAT, MaxSAT, and PB solvers, CardSAT-LS solves the most instances with the lowest PAR-2 score. Additionally, we integrate CardSAT-LS into exact solvers for phase selection, which leads to significant speedups.
Keywords:
Constraint Satisfaction and Optimization: Satisfiabilty
Search: Combinatorial search and optimisation
Search: Local search
