---
title: "Towards Cardinality-Aware Local Search for SAT with Cardinality Constraints"
authors:
  - "Shuli Hu"
  - "Dian Ling"
  - "Jiaqi Li"
  - "Minghao Yin"
doi: "10.24963/ijcai.2026/251"
url: "https://ijcai.org/proceedings/2026/251"
pdf: "https://ijcai.org/proceedings/2026/0251.pdf"
venue: "Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence"
year: 2026
pages: "2256-2264"
track: "Main Track"
keywords:
  - "Search: Combinatorial search and optimisation"
  - "Constraint Satisfaction and Optimization: Satisfiabilty"
  - "Search: Local search"
---

# 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*, pages 2256-2264. DOI: [10.24963/ijcai.2026/251](https://doi.org/10.24963/ijcai.2026/251)

## Abstract

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.