Towards Cardinality-Aware Local Search for SAT with Cardinality Constraints

1 Introduction

Satisfiability problem (SAT) is a basic and important constraint problem, and it constitutes a central paradigm for modeling and solving a wide range of real-world problems, including planning [Rintanen et al., 2006], scheduling [Horbach, 2010], and verification [Vizel et al., 2015]. Over the past decades, remarkable success has been achieved in solving techniques for SAT, including the complete solvers based on conflict-driven clause learning [Mull et al., 2022; Chowdhury et al., 2020; Biere and Fr¨ohlich, 2015] and incomplete methods such as stochastic local search [Hutter et al., 2002; Bailleux and Boufkhad, 2003; Cai et al., 2015].

∗Corresponding author.

These techniques played a crucial role in enabling SAT-based approaches to tackle large and complex real-world instances.

Although many aspects of the SAT solvers have changed, most modern solvers still use Conjunctive Normal Form (CNF) formulas as their input representation. However, many practical problems involve constraints that go beyond simple logical disjunctions [Bard et al., 2007; Ab´ıo and Stuckey, 2014]. For such problems, it is challenging for the users to find an appropriate encoding. Moreover, essential structural information captured by high-level constraints is hard to express at the clause level. Among these high-level constraints, cardinality constraints are particularly common in SAT problems, which assert the sum of a set of literals exceeds a given bound [Marques-Silva and Lynce, 2007]. Cardinality constraints arise naturally in any problems that require counting, such as those with resource or assignment limitations.

Despite the richer representations provided by Satisfiability Modulo Theories (SMT) and Pseudo-Boolean (PB) constraints, which offer more expressive modeling and stronger reasoning, eager approaches that translate constraints into SAT are still desirable in many practical settings. The reason is that in some domains higher-level reasoning is not always necessary, and eager solving can be surprisingly effective. For example, for bit-vectors the eager SMT solver performs well in practice [Niemetz and Preiner, 2023]. Besides, SAT solvers benefit from decades of intensive optimization, including efficient propagation, conflict-driven clause learning, and sophisticated heuristics, which make them highly competitive on large-scale instances. In this context, SAT with cardinality constraints, allowing cardinality constraints to be represented explicitly, bridges the gap between the pure CNF and fully general PB or SMT.

Many approaches for handling cardinality constraints have been proposed. A common approach is to encode cardinality constraints into CNF using dedicated coding, such as sequential counters[Sinz, 2005], cardinality networks[As´ın et al., 2009; As´ın et al., 2011], and totalizer[Bailleux and Boufkhad, 2003; Ogawa et al., 2013; Ignatiev et al., 2018]. While this enables the use of highly optimized SAT solvers, a well-known drawback is that many auxiliary variables and clauses are introduced, which can obscure the constraint's original structure [Wynn, 2018]. Interestingly, recent work by [Reeves et al., 2025] demonstrates that for such encodings, the ordering of literals often has a greater impact on solver performance than the choice of the encoding method itself. Another approach is using PB solvers, which handle cardinality constraints directly, including Stochastic Local Search (SLS) PB solvers [Lei et al., 2020; Lei et al., 2021; Chu et al., 2023] and exact PB solvers [Devriendt et al., 2021; Le Berre and Parrain, 2011]. However, a significant practical limitation is that PB solvers perform poorly when the input is provided in standard CNF format[Elffers and others, 2020]. Recently, [Reeves et al., 2024] has proposed an extension of CDCL with native propagation on cardinality constraints, which performed well on SAT formulas. Despite these advances, existing local search methods are not well-tailored to instances combining CNF clauses and cardinality constraints. This motivates our cardinality-aware local search approach.

Contributions. We present CardSAT-LS, a cardinalityaware local search solver for SAT with At-Least-K CNF constraints. It combines generalized preprocessing, a cardinalityaware scoring function, fake-backbone-based initialization, and adaptive flip/swap moves. Experiments on 814 benchmark instances show that it solves the most instances and achieves the best PAR-2 among 10 competing SAT, MaxSAT, and PB solvers, and it also accelerates exact solvers when used for phase selection.

2 Preliminaries

Let X = {x1, x2, . . . , xn} be a set of Boolean variables. A literal is either a variable xi (positive literal) or its negation ¬xi (negative literal). The phase of a literal indicates whether it is positive or negative. Let L = {l1, l2, . . . , lm}, and var(l) is to denote the corresponding variable of a literal. A clause is a disjunction of literals, and a Conjunctive Normal Form (CNF) F is a conjunction of clauses. A pure literal is a literal whose complement (the same variable with the opposite sign) does not appear anywhere in the formula.

An assignment α is a mapping from variables to truth values in {0, 1}, where 1 denotes true and 0 denotes false. An assignment α satisfies a positive literal l by setting α(var(l)) to 1, and satisfies a negative literal l by setting α(var(l)) to 0. An assignment falsifies a literal if the corresponding condition does not hold. An assignment α satisfies a clause if it contains at least one literal satisfied by α. A CNF F is satisfiable if and only if there exists an assignment that satisfies all clauses, and unsatisfiable otherwise.

A unit is a clause containing a single literal. Unit Propagation (UP) applies the following operation until a fixed-point: Given a CNF formula F , all unit clauses are collected and the assignment α is derived by setting each variable to satisfy its unit clause. That is, if the unit {xi} appears in F, we set xi to true; and if the unit {¬xi} appears in F, we set xi to false. All clauses satisfied by α are removed from F, and all literals falsified by α are removed from the remaining clauses. A conflict is detected if UP yields the empty clause (⊥).

2.1 Cardinality Constraints

A cardinality constraint over Boolean variables has the form ∑ri=1 xi ▷ k, where xi ∈ {0, 1}, ▷ ∈ {≥, ≤, =}, and k ∈ N. Such a constraint is satisfied by an assignment if the sum of the values of the variables satisfies the relation ▷k.

Since each literal l can be identified with its underlying variable var(l), we equivalently write cardinality constraints over literals in the form ∑ri=1 li ▷ k, where each li is a literal interpreted as a Boolean value in {0, 1}.

For clarity and without loss of generality, constraints of the form ∑ri=1 li ≤ k can be rewritten as ∑ri=1 ¬li ≥ r - k, since li + ¬li = 1 holds. Similarly, constraints of the form ∑ri=1 li = k can be rewritten as (∑ri=1 li ≥ k) ∧ (∑ri=1 ¬li ≥ r - k). Therefore, in the following we restrict our attention to At-Least-K (ALK) constraints of the form ∑ri=1 li ≥ k.

2.2 At-Least-KConjunctive Normal Form (KNF)

For the SAT with cardinality constraints, we adopt the same formulation of [Reeves et al., 2024]. Following its terminology, we refer to ALK constraints (∑ri=1 li ≥ k) as klauses, each consisting of a set of literals and a bound k. A standard clause can be viewed as a special case of a klause with bound k = 1, that is, the At-Least-One (ALO) constraint. A formula is in At-Least-K Conjunctive Normal Form (KNF) if it is a conjunction of klauses. Under the KNF representation, cardinality constraints are explicitly represented, enabling reasoning directly at the level of constraints rather than at the level of clauses. Note that CNF is a strict subset of KNF.

3 Cardinality-Aware Local Search for KNF

In this section, we introduce our proposed cardinality-aware local search for SAT with cardinality constraints represented in KNF. Firstly, the generalized UP and resolution are provided to simplify the formula in the preprocessing phase. Secondly, a novel score function combining cardinality violation and the make-break mechanism is introduced. Subsequently, an initialization based on fake-backbone variables is presented. Finally, we propose a unified framework that adaptively alternates between flip and swap operators.

3.1 Generalized UP and Resolution

Definition 1 (Generalized Unit). Given a klause c := ∑ri=1 li ≥ k, if k = |c|, where |c| is the number of literals in c, we say that c is a generalized unit.

Unit Propagation can be generalized to KNF via Definition 1, and the generalized UP is provided in Theorem 1.

Theorem 1 (Generalized UP). Given a generalized unit klause c := ∑ri=1 li ≥ k, it holds if li is true for all 1 ≤ i ≤ r.

Proof. The proof is straightforward: when k = |c|, satisfying klause c requires all of its literals to be true.

The process of Generalized UP is similar to original UP. After that, some variables' assignments could be fixed, and some klauses and literals can be removed to simplify the formula.

Theorem 2 (Generalized Resolution). Given two klauses c1 := y + ∑ri=1 xi ≥ k1 and c2 := ¬y + ∑tj=1 zj ≥ k2, if the sets of literals {xi}ri=1 and {zj}tj=1 are disjoint

({xi}ri=1 ∩ {zj}tj=1 = ∅), then their resolvent c with respect to y is given by:

where c remains a valid klause.

Proof. From c1 ∧ c2, adding the two inequalities yields:

Equation (2) holds due to the tautology y +¬y = 1. Since {xi}ri=1 ∩ {zj}tj=1 = ∅, the summation ∑ri=1 xi + ∑tj=1 zj contains no duplicated literals. Consequently, the resolvent c := c1 ⊗y c2 = ∑ri=1 xi + ∑tj=1 zj ≥ k1 +k2 -1 is a wellformed klause, confirming that c is a logical consequence of the resolution of c1 and c2.

We generalized the Resolution Checking (RC) [Chen et al., 2022], a variant of the Bounded Variable Elimination (BVE) [Biere, 2013] with stricter conditions, to the KNF setting. To address the time consumption of BVE, we employ a simple heuristic to decide whether to perform the elimination. Assume s(l) denotes the set of klauses in which literal l appears. For each variable x, if |s(x)| × |s(¬x)| ≤ |s(x)| + |s(¬x)|, we resolve s(x) with s(¬x) and check whether all resulting klauses are tautologies. If so, the clauses related to variable x can be removed.

During elimination, many pure literals could be produced, so we propose a generalized pure literal rule to simplify the formula again. The process is illustrated in Example 1.

Example 1. Given a KNF F = (¬x3 +¬x5 +¬x7 +¬x8 ≥ 2) ∧ (x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ ¬x2 ∨ x3) ∧ (x5 ∨ ¬x7), we could easily eliminate variable x1 since (x1 ∨ x2 ∨ x3) ⊗x1 (¬x1 ∨ ¬x2 ∨ x3) is always true. Thus, the simplified KNF F ′ = (¬x3 + ¬x5 + ¬x7 + ¬x8 ≥ 2) ∧ (x5 ∨ ¬x7).

Furthermore, we observe that ¬x3 is a pure literal (since x3 does not appear positively). According to the pure literal rule, we can safely set ¬x3 to true.

Substituting this assignment into the cardinality constraint (¬x3 +¬x5 +¬x7 +¬x8 ≥ 2) simplifies it to (¬x5 +¬x7 + ¬x8 ≥ 1). Thus, F ′ is further simplified to: (¬x5 + ¬x7 + ¬x8 ≥ 1) ∧ (x5 ∨ ¬x7)

The preprocessing algorithm based on the generalized UP and resolution is outlined in Algorithm 1, and described below. The algorithm first performs a generalized unit propagation (lines 2-9) based on Theorem 1; unlike the traditional UP, we decrement the bound k of a klause when a literal in it is assigned true and remove the klause if k = 0. After Generalized-UP, we apply the Generalized Resolution Check

Algorithm 1 Generalized-Preprocessing

Require: AKNF F Ensure: A simplified KNF F ′ 1: F ′ ←F 2: while ∃ generalized unit c do 3: ∀li ∈ c, li ← 1 4: ∀cj ∈ s(¬li), cj ← cj \ {¬li} 5: ∀cj ∈ s(li) , cj , kj ← cj \ {li} , kj -1 6: if kj = 0 then 7: ∀cj ∈ s(li), F ′ ← F ′ \ {cj} 8: end if 9: end while 10: for each variable x ∈ F ′ do 11: if x is the pure literal and x ∈ cj (resp. ¬x) then 12: x ← 1 13: cj , kj ← cj \ {x} , kj - 1 14: if kj ≤ 0 then 15: F ′ ←F ′ \ {cj} 16: end if 17: else if |s(x)| × |s(¬x)| ≤ |s(x)| + |s(¬x)| then 18: ∀ci ∈ s(x), ∀cj ∈ s(¬x), R ← R ∪ ci ⊗x cj 19: if ∀r ∈ R is tautology then 20: F ′ ← F ′ \ {c ∈ s(x) ∪ s(¬x) | k(c) = 1} 21: end if 22: end if 23: end for 24: return F ′

and Generalized Pure Literal Rule (line 10-23) as shown in Example 1. Note that the resolution is applied exclusively during preprocessing to simplify the formula while preserving its KNF structure. The resulting formula is then solved by CardSAT-LS local search procedure.

3.2 Scoring Function CombiningMake-break Mechanism and Violation

Scoring Function in SLS SAT Solver. Usually, SLS algorithms for SAT select a variable to flip according to scoring functions [Selman et al., 1994] based on the properties make(x) and break(x), which are the number of clauses that would become satisfied and unsatisfied by flipping a variable x. In this context, score(x) = ∑c∈Make(x) w(c) - ∑c∈Break(x) w(c), where Make(x) and Break(x) are the sets of clauses impacted by flipping x, and w(c) is the weight of clause c [Morris, 1993]. However, this scoring function has a drawback: it cannot measure the slack of cardinality constraints. In the following, we illustrate our intuition through a simple SAT instance with cardinality constraints.

Example 2. Let us consider a KNF instance, which consists of four clauses and one cardinality constraint: F = (x1 ∨ x2∨x3)∧(¬x1∨¬x4)∧(x2∨x5)∧(x3∨x6)∧(x1+x3+x4+ x5 + x6 ≥ 3), the current assignment is α = (0, 0, 0, 1, 0, 0) and all weights of klauses are 1. Calculating the scores, we find that score(x2) = 2 and score(x3) = 2.

Example 2 shows a limitation: although flipping x3 is superior to flipping x2 for satisfying the cardinality constraint,

Algorithm 2 Initialization

Ensure: An assignment α 1: α← ∅ 2: for each variable xi ∈ F do 3: if time stamp[xi] > thresbb then 4: α←α∪ {xi ↦→ 0} 5: else 6: α←α∪ {xi ↦→ backbone[xi]} 7: end if 8: end for 9: return α

the algorithm cannot distinguish them and picks one randomly.

To address this issue, we introduce a metric to quantify the satisfaction level of cardinality constraints. Specifically, we adapt the concept of violation degree from SLS PBO solvers [Lei et al., 2021] as a scoring component. Integrating this metric with the traditional make-break mechanism, we construct a novel scoring function. It consists of two parts: (1) scorem b is to evaluate the impact on the normal clause by flipping x; (2) scorecard is to evaluate the decrement of the violation of cardinality constraints.

where viol(c) = max (0, k - ∑ri li). Revisiting Example 2, based on the new scoring function, score(x2) = 2 and score(x3) = 3.

Like state-of-the-art solvers, we employ dynamic weighting at the klauses level to escape local optima. The rules are as followings.

• Initialization rule: at the start of the search process, the weight of each klause c is initialized as 1, i.e., w(c) := 1.
• Update rule: when the search is trapped in a local optimum (there is no variable whose score value is greater than 0), for each falsified klause c, w(c) := w(c) + 1.

3.3 Initialization Based on Fake-Backbone Variables

In traditional SLS SAT solvers, initialization is often overlooked, with randomized assignments typically yielding satisfactory performance. However, in SLS PBO solvers, this paradigm shifts toward an all-zero initialization [Lei et al., 2021]. Nevertheless, we observe that preprocessing significantly biases the phase selection of variables. To balance diversity with the exploitation of historical search information during restarts, we draw inspiration from the target phase strategy in CaDiCaL [Biere, 2017] (which tracks the longest conflict-free assignment sequence). Consequently, we propose a fake-backbone randomized initialization strategy to substantially enhance solver performance.

Algorithm 3 The CardSAT-LS Algorithm

Require: AKNF F Ensure: "SAT" and its model, or "Unknown" 1: F ←Generalized-Preprocessing(F) 2: while no terminating criteria are met do 3: α←Initialization() 4: ∀c ∈ F, w(c) := 1 5: non improved← 0 6: for step ← 0; step < L; step + + do 7: if ̸ ∃ unsatisfied klauses then 8: return {"SAT", α} 9: end if 10: if the number of satisfied klauses increases then 11: non improved← 0 12: end if 13: non improved←non improved + 1 14: if ∃satisfied cardinality constraints ∧ non improved > thresn i ∧ p < pswap then 15: Swap-Operator(step,α) 16: else 17: if D := {x|score(x) > 0 ∧ cc[x] > 0} ̸= ∅ then 18: v ← a variable in D with the highest score 19: else 20: update klauses weights by the weighting rules 21: if ∃ unsatisfied klauses then 22: c ← a random unsatisfied klause 23: v ← the variable whose literal is false in c with the highest score 24: end if 25: end if 26: flip(v), time stamp[v] = step 27: end if 28: end for 29: backbone←α 30: end while 31: return "Unknown"

Given that SLS algorithms lack a deterministic mechanism to identify actual backbones, our initialization strategy is predicated on a simple yet effective heuristic assumption: if a variable's last flip occurred at a very early stage of the search (i.e., its timestamp is small), it suggests that the variable's current assignment is likely correct and should remain unaltered. Thus, we retain the assignments of these variables to exploit historical search knowledge while restarting. For the first initialization, we employ a traditional randomized approach to ensure a robust and unbiased starting point for the solver. The initialization is as detailed in Algorithm 2.

3.4 The CardSAT-LS Algorithm

We develop a new SLS algorithm named CardSAT-LS, which is based on the main ideas proposed in previous sections. CardSAT-LS adopts the iterated local search with Configuration Check [Cai et al., 2015] to avoid revisiting the same variable frequently. The pseudo-code is outlined in Algorithm 3.

CardSAT-LS starts by performing generalized preprocessing to simplify the formula (Line 1). It then iteratively executes the local search procedure, adaptively alternating be-

Algorithm 4 Swap-Operator

Require: Current step step, assignment α

• 1: c ← select a satisfied cardinality constraint randomly
• 2: D := {x|score(x) > 0 ∧ cc[x] > 0 ∧ (x ∈ c ∨ ¬x ∈ c)}
• 3: vin ← a variable in D with the highest score and α(x) is 1;
• 4: vout ← a variable in D with the highest score andα(x) is 0;
• 5: flip(vin) and flip(vout)
• 6: time stamp[vin] = step, time stamp[vout] = step

tween Flip and Swap operators until a stopping criterion is met. In the local search process, an initial assignment is generated by the method described in Section 3.3 (Line 3). CardSAT-LS then initializes the weights of all klauses to 1. The algorithm then enters the main search procedure (Lines 6-28).

In each search step, our algorithm selects and flips variables based on the following logic: (I) If there exists satisfied cardinality constraints but the search has stagnated, the algorithm invokes the Swap Operator described below with a probability pswap. (II) If the swap condition is not met, the algorithm checks the variable set D that satisfy score(x) > 0 and configuration check (cc[x] > 0). If D is not empty, the variable with the highest score is selected for flipping, breaking ties by preferring the variable that has been flipped least recently. (III) When D is empty, indicating that the search is trapped in a local optimum, the algorithm updates the weights of all klauses according to the dynamic weighting rules. After the update, if unsatisfied klauses remain, the algorithm randomly picks an unsatisfied klause c. To reduce the violation, it selects the variable in c whose literal is false under the current assignment and which possesses the highest score. Note that our algorithm employs the BMS (Best fromMultiple Selections) strategy [Cai et al., 2017] to select variables and klauses. After flipping or swapping, CardSAT-LS will update the score and cc of those affected variables.

Finally, the search continues until a satisfying assignment α is found (returning "SAT") or the step limit L is reached.

A New Swap-Operator. Compared to standard clauses, cardinality constraints impose significantly more stringent restrictions on variables, which often leads the local search to become trapped in local optima. Specifically, once a cardinality constraint is exactly satisfied, the solver encounters an issue: it becomes reluctant to flip variables that would violate the constraint, even if such flips could potentially satisfy a greater number of clauses. To mitigate this, we introduce a swap operator. This operator is specifically triggered when the search stagnates in a local optimum while there exists a satisfied cardinality constraint, as detailed in Lines 14-15 of Algorithm 3.

4 Experimental Evaluation

In this section, we introduce the experimental preliminaries and our results. We compare CardSAT-LS with 10 state-ofthe-art solvers to verify its effectiveness. Then, we conduct the experiment to analyze the effectiveness of main ideas.

Finally, we integrate CardSAT-LS into complete solvers for phase selection, which leads to significant speedups.

Benchmarks. We evaluate our algorithm on 5 benchmarks, including 2 competition benchmarks and 3 real-world application benchmarks.

• MaxSAT24: The benchmark is from the latest 2024 MaxSAT competition unweighted track [Berg et al., 2024]. We generate 368 satisfiable SAT problems by making the cardinality constraint's bound the known optimum.
• SAT25: This benchmark is derived from the main track of the latest 2025 SAT Competition [Codel et al., 2025]. We applied the cardinality extraction procedure [Reeves et al., 2024] to each formula, and generated 273 instances (82 known UNSAT instances) with explicit cardinality constraints.
• DES: 120 instances are from diagnosis of DiscreteEvent System problems [Anbulagan and Grastien, 2009] 1 , with 14,621 to 636,593 variables and 3,320 to 142,474 constraints.
• MVC: 117 Minimum Vertex Cover instances are from the Second DIMACS Challenge and large real-world graphs 2 , with 34 to 58,790,782 variables and 112 to 150,998,977 constraints.
• WSNO: 18 instances are from Wireless Sensor Network Optimization (WSNO) [Kov´asznai et al., 2018; Kov´asznai et al., 2019] 3 , encoded following [Lei et al., 2021] into KNF, with 58,580 to 2,311,113 variables and 214,679 to 26,701,722 constraints.

State-of-the-Art Competitors. We compare our algorithm against 10 state-of-the-art algorithms including SAT, MaxSAT and Pseudo-Boolean solvers.

• CCDCL [Reeves et al., 2024]: a CDCL-based SAT solver built on CaDiCaL [Biere, 2017] with native cardinality constraint propagation.
• CCAnr [Cai et al., 2015]: a local search SAT solver with configuration checking.
• TaSSAT [Chowdhury et al., 2024]: the best local search SAT solver that effectively solves hard combinatorial problems.
• YalSAT [Biere, 2017]: an efficient implementation of the ProbSAT local search algorithm.
• WalkSATlm [Cai et al., 2013]: an improved version from the famous WalkSAT(SKC) algorithm.
• RoundingSAT [Devriendt et al., 2021]: an exact PBO solver combining core-guided search with cutting planes reasoning.
• NuPBO [Chu et al., 2023]: a local search PBO solver, incorporating the new scoring function and weighting scheme.

1 http://grastien.net/ban/data/cc/

2 https://lcs.ios.ac.cn/%7Ecaisw/graphs.html

3 https://lcs.ios.ac.cn/%7Ecaisw/Resource/LS-PBO/benchmark/

• DLS-PBO [Chen et al., 2024]: a local search PBO solver, combining a dynamic scoring function.
• NuPBO-DeepOPT+ [Zhao et al., 2025]: the state-ofthe-art local search solver for PBO.
• Open-WBO [Martins et al., 2014]: a complete unsatisfiable-core-based MaxSAT solvers.

Experimental Setup. CardSAT-LS 4 is implemented in C++, and compiled with g++ (version 11.4.0) using the option "-O3 -flto". All the experiments were performed on a workstation under the operating system Ubuntu 22.04.5, with the Intel(R) Xeon(R) Platinum 8260 2.40GHz CPU and 1TB RAM. The cut-off time for all solvers is 3600 seconds. Each run was allocated a memory limit of 30 GB, following the SAT Competition rules.

For parameter tuning, we employed Sequential Modelbased Algorithm Configuration (SMAC) [Lindauer et al., 2022], conducting the tuning on 300 instances randomly selected from all the benchmarks, with a time limit set to 300 seconds. The parameter values obtained after tuning are as follows: the maximum step L is 109 ; the probability of calling swapping operator pswap is 0.32; the threshold for fakebackbone thresbb is 5076; the threshold of not improved steps thresn i is 122. For reproducibility, we set all randomization seeds to 20.

4.1 Results on Competition Benchmarks

Table 1 presents the comparative performance of CardSATLS against 10 state-of-the-art competitors on five benchmarks, comprising 3 exact solvers and 7 SLS solvers. For each solver, we report the number of solved instances and PAR-2 score. PAR-2 is the sum of runtime over all instances, where timeouts and memory-outs are penalized by 2 × 3600 seconds, divided by the total number of instances.

On the MaxSAT24 benchmark, CardSAT-LS exhibits dominant performance, solving a total of 291 instances. This surpasses the best exact solver, CCDCL (258 solved), and the leading LS competitor, DLS-PBO (243 solved). In terms of solving efficiency, CardSAT-LS achieves the lowest PAR-2 score of 1605.58, 30.2% lower than the second-best score.

On SAT25, all three exact solvers solve more instances than the SLS solvers. Among SLS solvers, CardSAT-LS and CCAnr tie for second in solved count (46 each), behind TaSSAT (61). The corresponding PAR-2 scores are 5606.86, 5523.68, and 5030.42, respectively, indicating that SAT25 remains a comparatively difficult benchmark for CardSAT-LS.

Across all 814 instances, Figure 1 shows that the cumulative curve of CardSAT-LS stays above all competitors throughout the measured range. It solves 234, 348, 456, and 536 instances within 1, 10, 100, and 1000 seconds, versus the best competing counts of 190, 296, 399, and 481. At the cutoff, it solves 557 instances, 32 more than CCDCL, and its aggregate PAR-2 of 2369.06 is 12.5% lower than CCDCL's 2708.11.

4 https://github.com/virgiling/CardSAT-LS

4.2 Results on Real-World Application Benchmarks

Table 1 shows that CardSAT-LS achieves or ties the highest solved count on all three application benchmarks. On DES, both CardSAT-LS and TaSSAT solve all 120 instances; their PAR-2 scores are 61.81 and 28.77, respectively, while TaSSAT solves no WSNO instance. On MVC, CardSAT-LS solves 82 instances, four more than TaSSAT and 31 more than the best exact solver; its PAR-2 of 2213.67 is 10.9% lower than the second-best score of NuPBO. On WSNO, CardSATLS solves all 18 instances and achieves the lowest PAR-2 of 13.02, followed by CCDCL at 15.19. These results demonstrate broad coverage across the three application domains without implying uniform dominance on every metric.

4.3 Analysis on the Underlying Ideas

Figure 2 compares five CardSAT-LS configurations on all 814 benchmark instances:

• CardSAT-LS+P+B+S: retains all three strategies.
• CardSAT-LS-P-B-S: disables P, B, and S and uses NuPBO's all-zero initialization.
• CardSAT-LS+P-B-S: retains only generalized preprocessing.
• CardSAT-LS-P+B-S: retains only fake-backbone initialization.
• CardSAT-LS-P-B+S: retains only the swap operator.

As shown in Figure 2, each single-strategy variant improves both metrics over the base variant (486 solved, PAR2 2999.67). Preprocessing gives the largest individual gain, solving 549 instances and reducing PAR-2 to 2453.64, an increase of 63 solved instances and an 18.2% PAR-2 reduction. Fake-backbone initialization and the swap operator also improve the base variant, reaching 521/2682.85 and 527/2673.94, respectively. Thus, every strategy contributes individually, and their combination provides an additional empirical gain.

4.4 Integration with CCDCL

We integrated our proposed local search algorithm into the CCDCL framework ( CCDCL+CardSAT-LS, CCDCL-LS in short), specifically employing it to guide the solution search and determine phase selection during each walk iteration. The comparative results are presented in Figure 3.

Across all 896 instances, CCDCL-LS solves 748 versus 589 instances and lowers PAR-2 from 2641.04 to 1351.61.

5 Conclusions and FutureWork

This paper proposes a cardinality-aware local search framework for solving SAT with cardinality constraints. First, we introduced a generalized preprocessing technique along with an initialization method specifically designed to cooperate with it. Furthermore, we proposed a cardinality-sensitive scoring function and a novel swap operator which effectively guides the direction of search. Based on these ideas, we developed a new SLS solver named CardSAT-LS. Across 814 instances, CardSAT-LS achieves the highest solved count and lowest aggregate PAR-2 among the 11 evaluated solvers. Additionally, we integrate CardSAT-LS into exact solvers for phase selection, which leads to significant speedups. For future work, we would like to develop more efficient heuristic strategies and explore the effect of instance features on the performances of different categories of SAT with cardinality constraints.

Acknowledgments

This work was supported by the National Natural Science Foundation of China (Grant Nos. 62106040, 62532014), Jilin Science and Technology Association (Grant No. QT202320), and the Science and Technology Development Plan Project of Jilin Province of China (Grant No. 20240602108RC).