A Study of Parallel Continuous Local Search

# A Study of Parallel Continuous Local Search
Source: [https://arxiv.org/html/2606.06656](https://arxiv.org/html/2606.06656)
\\hideLIPIcs

School of Computing, Australian National University, Canberra, Australia\.cody\.christopher@anu\.edu\.auhttps://orcid\.org/0000\-0001\-8444\-2292 School of Computing, Australian National University, Canberra, Australia\.charles\.gretton@anu\.edu\.auhttps://orcid\.org/0000\-0001\-9803\-0168\\CopyrightCody J Christopher and Charles Gretton\\ccsdesc\[500\]Mathematics of computing Combinatorial optimization\\ccsdesc\[500\]Mathematics of computing Solvers\\ccsdesc\[500\]Mathematics of computing Nonconvex optimization\\supplement\\afsimplementation withApache\-2\.0/GPL\-2\.0\-or\-laterlicenses:\\supplementdetails\[linktext=, cite=, subcategory=Source Code, swhid= \]Softwarehttps://github\.com/cjchristopher/accelerated\-fourier\-sat/\\EventEditors\\EventNoEds0\\EventLongTitle\\EventShortTitle\\EventAcronym\\EventYear\\EventDate\\EventLocation\\EventLogo\\SeriesVolume\\ArticleNo

###### Abstract

We study parallel Continuous Local Search \(CLS\) as a solution approach for Boolean satisfiability problems with symmetric pseudo\-Boolean \(PB\) constraints\. Here, thenn\-variable PB\-satisfiability problem is relaxed to a continuous optimisation problem with a differentiable objective function on annn\-dimensional hypercube\. For satisfiable instances, the global minimisers of this optimisation problem correspond to satisfying assignments of the SAT problem at hand\. We present several novel findings via empirical experiments: \(i\) redundant constraints can inhibit rather than accelerate convergence; \(ii\) CLS shows promise as a sub\-solver in hybridised settings, quickly completing partial assignments; and \(iii\) local search rapidly converges to a stable distribution of solution quality \(i\.e\., degree of satisfaction\), due to saddle\-dense objectives where additional solver steps yield diminishing returns\. Our findings inform practical uses of CLS for SAT on modern accelerator hardware\.

###### keywords:

Satisfiability, pseudo\-Boolean, SAT Solver, continuous local search, combinatorial optimization, hardware acceleration

## 1Introduction

Continuous local search \(CLS\) offers an alternative that is inherently parallelisable and amenable to GPU acceleration\. CLS relaxes Boolean variables to real values on\[−1,1\]\[\-1,1\]via the Walsh\-Fourier expansion\[odonnell14\], reformulating satisfaction as bounded non\-convex continuous optimisation\. This approach was formalised inFourierSAT\[kyrillidis2021solving\]and extended for GPU computation inFastFourierSAT\[cen2025massively\]\. A companion paper\[christopher2026afsat\]describes the engineering and performance of our solver Accelerated Fourier SAT \(\\afs\), used throughout this work for empirical evaluation\. We make the following contributions:

1. \(a\)We analyse the representational advantage of native psuedo\-Boolean \(PB\) encodings for CLS over CNF translations \(§[2\.4](https://arxiv.org/html/2606.06656#S2.SS4)\)\.
2. \(b\)We present closed\-form Fourier coefficient derivations for all symmetric PB constraint types of practical interest \(Appendix[A](https://arxiv.org/html/2606.06656#A1)\)\.
3. \(c\)We provide empirical case studies revealing novel phenomena in CLS behaviour, including gradient interaction effects, partial assignment solving, and convergence profiling \(§[3](https://arxiv.org/html/2606.06656#S3)\)\.

## 2Background

### 2\.1Walsh\-Fourier Transformation

We review analytical properties of Boolean functions, notably that they can be relaxed into continuous functions inℝ\\mathbb\{R\}, with\{True,False\}↦\{−1,1\}\\left\\\{\\texttt\{True\},\\texttt\{False\}\\right\\\}\\mapsto\\left\\\{\-1,1\\right\\\}\. For a Boolean formulaϕ:\{⊤,⊥\}n↦\{⊤,⊥\}\\phi:\\left\\\{\\top,\\bot\\right\\\}^\{n\}\\mapsto\\left\\\{\\top,\\bot\\right\\\}, a continuous relaxation isRelϕ:\[−1,1\]n↦\[−1,1\]\\text\{Rel\}\_\{\\phi\}:\[\-1,1\]^\{n\}\\mapsto\[\-1,1\]\.\[−1,1\]n\[\-1,1\]^\{n\}is the convex Boolean hypercube𝒬n\\mathcal\{Q\}^\{n\}\. The Walsh\-Fourier expansion\[odonnell14,kyrillidis2021solving\]is such a relaxation:

FEϕ​\(𝐗\)=def∑S∈2𝐗f^​\(S\)​∏xi∈Sxi\\texttt\{FE\}\_\{\\phi\}\(\\mathbf\{X\}\)\\stackrel\{\{\\scriptstyle\\text\{def\}\}\}\{\{=\}\}\\sum\_\{S\\in 2^\{\\mathbf\{X\}\}\}\\hat\{f\}\(S\)\\prod\_\{x\_\{i\}\\in S\}x\_\{i\}\(1\)𝐗\\mathbf\{X\}is the set ofnnvariables andf^​\(S\)\\hat\{f\}\(S\)are the*Fourier coefficients*at subsetS⊆𝐗S\\subseteq\\mathbf\{X\}\.FEϕ\\texttt\{FE\}\_\{\\phi\}is a multi\-linear polynomial—a linear combination of*elementary symmetric polynomials*\(ESP\)\.

ein=∑1≤j1<j2<…<ji<n∏k=1ixjke\_\{i\}^\{n\}=\\sum\_\{1\\leq j\_\{1\}<j\_\{2\}<\\ldots<j\_\{i\}<n\}\{\\prod\_\{k=1\}^\{i\}\{x\_\{j\_\{k\}\}\}\}\(2\)
Computing Fourier coefficients for general Boolean formulae may be exponentially expensive\. However, for*symmetric*constraints—those whose truth depends*only on how many*literals are true—the symmetry reduces the number of distinct coefficients ton\+1n\+1, and closed\-form solutions exist\[kyrillidis2021solving\]\. The general coefficient formula for symmetric constraints is:

f^​\(S\)=\{12n​∑i=0n\(ni\)​s​pi\|S\|=0g​\(ρ\)\[ρ\|S\|−1\]\(n−1\|S\|−1\)​2n−1\|S\|≠0\\displaystyle\\hat\{f\}\(S\)=\\begin\{dcases\}\\frac\{1\}\{2^\{n\}\}\\sum\_\{i=0\}^\{n\}\\binom\{n\}\{i\}sp\_\{i\}&\\left\\lvert S\\right\\rvert=0\\\\ \\frac\{g\(\\rho\)\_\{\[\\rho^\{\\left\\lvert S\\right\\rvert\-1\}\]\}\}\{\\binom\{n\-1\}\{\\left\\lvert S\\right\\rvert\-1\}2^\{n\-1\}\}&\\left\\lvert S\\right\\rvert\\neq 0\\end\{dcases\}\(3\)wheres​pi=−1sp\_\{i\}=\-1ifffis true wheniivariables are true and11otherwise;g​\(ρ\)=∑i=0n−1di​\(n−1i\)​\(1\+ρ\)n−i−1​\(1−ρ\)ig\(\\rho\)=\\sum\_\{i=0\}^\{n\-1\}d\_\{i\}\\binom\{n\-1\}\{i\}\(1\+\\rho\)^\{n\-i\-1\}\(1\-\\rho\)^\{i\}; anddi=12​\(s​pi−s​pi\+1\)d\_\{i\}=\\frac\{1\}\{2\}\(sp\_\{i\}\-sp\_\{i\+1\}\)is the discrete derivative of the spectrum\. We provide closed form solutions in Appendix[A](https://arxiv.org/html/2606.06656#A1)\.

### 2\.2Pseudo\-Boolean Representation

Conjunctive normal form \(CNF\) constrains each clause to be a disjunction of literals:

ϕC​N​F=⋀Ck∈ϕ\(⋁li∈Cli\)\\phi\_\{CNF\}=\\bigwedge\_\{C\_\{k\}\\in\\phi\}\{\\left\(\\bigvee\_\{l\_\{i\}\\in C\}\{l\_\{i\}\}\\right\)\}\(4\)Many problems are more naturally expressed using*pseudo\-Boolean*\(PB\) constraints of the form∑i=1nci​li​ℛ​k\\sum\_\{i=1\}^\{n\}c\_\{i\}l\_\{i\}\\ \\mathcal\{R\}\\ k, whereℛ\\mathcal\{R\}is a comparison operator,cic\_\{i\}are coefficients, andkkis a threshold\[barth95\]\. Important special cases—all symmetric with unitary coefficients—include at\-most\-one \(AMO\), exactly\-one \(EO\), exactly\-kk\(EK\) not\-all\-equal \(NAE\), exclusive\-or \(XOR\), and cardinality\-kk\(CARD\) constraints\. Reduction of these constraints to CNF can be exponential naïvely, and polynomial encodings introduce auxiliary variables and clauses\[sinz2005towards,bailleux2003efficient,warners1998linear,10\.1007/978\-3\-031\-95973\-8\_8\]\.

### 2\.3Satisfaction as Optimisation

For a formulaϕ\\phidecomposed intommsymmetric constraintsC1,…,CmC\_\{1\},\\ldots,C\_\{m\}over variables𝐗\\mathbf\{X\}, the sound sum\-of\-expansions yields a continuous objective\[kyrillidis2021solving\]:

min𝐗​∑k=1mFECk​\(𝐗\)​subject to​𝐗∈𝒬n\\min\_\{\\mathbf\{X\}\}\\sum\_\{k=1\}^\{m\}\\texttt\{FE\}\_\{C\_\{k\}\}\(\\mathbf\{X\}\)\\text\{ subject to \}\\mathbf\{X\}\\in\\mathcal\{Q\}^\{n\}\(5\)A satisfying assignment is achieved when∑kFECk​\(sign​\(𝐗\)\)=−m\\sum\_\{k\}\\texttt\{FE\}\_\{C\_\{k\}\}\(\\texttt\{sign\}\(\\mathbf\{X\}\)\)=\-m\. This non\-convex, differentiable formulation motivates projected gradient descent \(PGD\), with the DFT enabling fully vectorised evaluation on GPU accelerators\[cen2025massively\]\.

A remark on an important structural property: since every multi\-linear polynomial is harmonic \(trivial Laplacian\), all critical points in the interior of𝒬n\\mathcal\{Q\}^\{n\}are saddle points\[kyrillidis2021solving\]\. Local and global minima exist only at the boundary, but the interior is proliferated with saddle points at which first\-order methods like PGD can stall\.

### 2\.4Representational Advantage of PB Encodings

The Walsh\-Fourier expansion preserves the native variable count and constraint count of PB\-encoded problems, in contrast to CNF translations which typically inflate both\. In Appendix[A](https://arxiv.org/html/2606.06656#A1)\), Table[2](https://arxiv.org/html/2606.06656#A2.T2)summarises the asymptotic costs\.

The Fourier expansion maintains a representational advantage since no auxiliary variables or additional constraints are required; the dominant coefficient computation cost is incurred once and depends only on the constraint parametersnnandkk\.

Problem \(Size\)CNF TranslationWalsh\-FourierVarsClausesVarsConstraintsRamsey 3C, 13N258714183234276Ramsey 3C, 16N455227032360411Costas Array 5x59759097245Costas Array 10x10712106227123434Costas Array 15x15257761980257718825Costas Array 20x205872196367587257289Sudoku 9x97293257729341Table 1:Variable and clause counts: Walsh\-Fourier vs\. CNF encodings for problems with native PB formulations\. Bold underlined values indicate outright smaller counts\.Table[1](https://arxiv.org/html/2606.06656#S2.T1)illustrates this advantage on concrete problem instances\. For Ramsey colouring problems withEOconstraints, the Walsh\-Fourier encoding reduces both variable and clause counts by an order of magnitude over CNF\. For Costas array problems, variable counts are preserved while clause counts are substantially reduced\.

This representational advantage is significant beyond mere compactness\. Resolution proof systems—and thereby CDCL procedures—can find PB constraints encoded in CNF challenging\[10\.1145/7531\.8928\], while systematic search tailored to PB constraints should theoretically be stronger\[COOK198725\]\. Practical realisation of this advantage in systematic search, however, remains difficult\[10\.1007/978\-3\-319\-94144\-8\_18,10\.1007/978\-3\-319\-94144\-8\_5\]\. CLS provides an alternative avenue for exploiting native PB encodings on accelerator hardware\.

## 3Case Studies

We present three case studies that reveal distinct aspects of CLS behaviour\. All experiments use\\afson NVIDIA Tesla V100 GPUs; see the companion tool paper\[christopher2026afsat\]for full experimental setup details\.

### 3\.1Ramsey Colouring: Gradient Interactions and Encoding Effects

A Ramsey colouring of a complete graphG=\(V,E\)G=\(V,E\)with coloursCCis an edge colouring containing no monochromatic triangles, amongst other conditions\[Kowalski2015,Alm2016401AB,Alm2019\]\. Whether colourings exist for\|C\|∈\{8,13\}\|C\|\\in\\\{8,13\\\}remains open\.

We study a*balanced assignment*relaxation requiring each vertex to have equal edge\-colour distribution\. In PB\-SAT:

⋀\{∀v∈V,∑i∈Cc​\(v,i\)=1∀v∈V,∀i∈C,∑v′∈V∖vc​\(v,i\)≥\|V\|−1\|C\|\\displaystyle\\bigwedge\\begin\{dcases\}\\forall v\\in V,&\\;\\;\\sum\_\{i\\in C\}\{c\(v,i\)\}=1\\\\ \\forall v\\in V,\\forall i\\in C,&\\sum\_\{v^\{\\prime\}\\in V\\setminus v\}\{c\(v,i\)\}\\geq\\frac\{\\left\\lvert V\\right\\rvert\-1\}\{\\left\\lvert C\\right\\rvert\}\\end\{dcases\}Here theEOconstraint ensures each edge gets exactly one colour, and cardinality constraints enforce balancing\. With this encoding,\\afsfinds colourings near\-instantly for\(\|V\|,\|C\|\)=\(16,3\)\(\|V\|,\|C\|\)=\(16,3\)\. We note that\(\|V\|,\|C\|\)=\(16,4\)\(\\left\\lvert V\\right\\rvert,\\left\\lvert C\\right\\rvert\)=\(16,4\)reaches constraint lengths close to the practical floating\-point ceiling \(n≈50n\\approx 50\), while global cardinality constraints on edges \(120 literals for\(16,3\)\(16,3\)\) are well beyond it, necessitating per\-vertex decomposition\.

#### 3\.1\.1Redundant Constraint Effect

An alternative encoding decomposes theEOconstraint as a disjunction plus a cardinality over negated literals:CARD≥2​\(¬𝐱\)​\+OR​\(𝐱\)\\texttt\{CARD\}\_\{\\geq 2\}\(\\lnot\\mathbf\{x\}\)\\texttt\{\+OR\}\(\\mathbf\{x\}\)\. We combine both encodings—EOand the decomposition—in a single problem\. SinceCARD≥2​\+OR=EO−1\\texttt\{CARD\}\_\{\\geq 2\}\\texttt\{\+OR\}=\\texttt\{EO\}\-1, the combination is equivalent to2⋅EO−12\\cdot\\texttt\{EO\}\-1, doubling the gradient magnitude of the edge\-colouring constraints\.

![Refer to caption](https://arxiv.org/html/2606.06656v1/x1.png)Figure 1:Evaluation, slope, and gradients of EO,CARD≥2​\(¬𝐱\)\\text\{CARD\}\_\{\\geq 2\}\(\\lnot\\mathbf\{x\}\), and OR constraints in 3 variables\.Counterintuitively, this doubled gradient steepness*inhibits*convergence: CLS succeeds approximately once per hundred runs \(vs\. near\-instant success otherwise\)\. Failed solutions typically violate 1–3 balancing constraints while satisfying all edge\-colouring constraints\.

We hypothesise a damped\-oscillator mechanism:

1. \(a\)Satisfying assignments occupy a tiny fraction of the hypercube vertices\. Edge\-colouring constraints are satisfied at specific corners \(Figure[1](https://arxiv.org/html/2606.06656#S3.F1)\)\.
2. \(b\)To satisfy remaining balancing constraints, literals must be flipped, requiring traversal away from the currently occupied corner\.
3. \(c\)The gradient field near satisfied vertices of the edge\-colouring constraints strongly attracts back toward the corner\. With doubled encoding, this attractive force is doubled\.
4. \(d\)The opposing gradient from unsatisfied balancing constraints is overwhelmed, causing the assignment to oscillate with decreasing amplitude and converge at the current \(non\-satisfying\) position\.

![Refer to caption](https://arxiv.org/html/2606.06656v1/x2.png)Figure 2:3D surface of evaluations forEO,CARD≥2​\(¬𝐱\)\\text\{\{CARD\}\}\_\{\\geq 2\}\(\\lnot\\mathbf\{x\}\), andORin 3 variables with one variable fixed at±1\\pm 1and0\.We further observe \(Figure[2](https://arxiv.org/html/2606.06656#S3.F2)\) that theEOconstraint exhibits a plateau at the all\-true corner \(all literals=−1=\-1\), where the gradient magnitude is small\. This creates a region from which PGD may struggle to escape, as the small step size satisfies convergence criteria prematurely\.

These findings suggest that:

- •CLS benefits from*minimal*encodings, consistent with the representational advantage of native PB formulations\.
- •Adaptive constraint weighting—informed by per\-constraint gradient magnitudes—is a promising direction for improving CLS on problems with structural symmetry\.

### 3\.2Hard Random 3\-SAT: Partial Assignment Completion

We evaluate CLS on hard random satisfiable 3\-SAT instances from the 2007 SAT Competition,111[https://satisfiability\.org/competition/2007/](https://satisfiability.org/competition/2007/)with 450–650 variables at the clause\-to\-variable phase transition ratio of≈4\.26\\approx 4\.26\[Cheeseman:1991:WRH,doi:10\.1126/science\.1073287\]\. These instances are solved rapidly byDagster\[10\.1007/978\-3\-031\-20862\-1\_6\], which incorporatesgNovelty\+\[DBLP:journals/jsat/PhamTGS08\]\.

CLS alone does not solve any of these instances\. To determine what support is needed, we fix a partial assignment of a known satisfying assignment and allow CLS to complete the remainder, simulating integration with a systematic solver\.

![Refer to caption](https://arxiv.org/html/2606.06656v1/x3.png)Figure 3:Time to solution for hard random 3\-SAT instances \(400–650 variables\) with increasing partial assignment lengths\.Figure[3](https://arxiv.org/html/2606.06656#S3.F3)shows that\\afscan complete solutions once1515–20%20\\%of variables are fixed, with monotonically decreasing solution time as the partial assignment lengthens\. This on\-average monotonic behaviour is significant: it means intuitions about when and how to deploy CLS as a sub\-solver can be relied upon, opening the door to integrated architectures where systematic search provides partial assignments that CLS completes on accelerators\. This is particularly relevant for \#SAT procedures that must enumerate completions of partial assignments\.

### 3\.3Costas Arrays: Convergence Profile Analysis

A Costas array is a set ofnnpoints in ann×nn\\times ngrid with exactly one point per row and column, and all displacement vectors distinct\[10\.1007/978\-3\-031\-20862\-1\_6\]\. Whether arrays exist atn∈\{32,33\}n\\in\\\{32,33\\\}are open problems\[5464772\]\. Forn≤6n\\leq 6,\\afsfinds all Costas solutions \(with duplication\)\. Forn≥7n\\geq 7, solution\-finding drops substantially; beyondn≥8n\\geq 8, none are found without assistance\.

We discover distinct convergence profiles that depend on the fraction of variables assigned\. These profiles have direct implications for solver parameterisation—specifically, the maximum descent steps hyper\-parameter\.

![Refer to caption](https://arxiv.org/html/2606.06656v1/x4.png)Figure 4:Costas\-15 \(≈\\approx66% assigned\): We show a heatmap view of a 3D histogram, and the component 2D histograms flanking above \(iterations taken to converge\) and left \(number of constraints unsatisfied\)\. The top\-right quadrant shows the correlation between the count of unsatisfied constraints and the energy of the evaluation\.For a high partially assigned regime \(≈\\approx66% assigned\), Figure[4](https://arxiv.org/html/2606.06656#S3.F4)shows a unimodal distribution where nearly all starting assignments converge well before the maximum step limit\. Solution quality is normally distributed and uncorrelated with the number of steps taken\. Comparing this to a low partially assigned regime \(≈\\approx10% assigned\), Figure[5](https://arxiv.org/html/2606.06656#S3.F5)shows a qualitatively different profile: a substantial fraction of initial assignments reach the maximum step limit \(300\) without converging\. The quality of unconverged assignments is statistically indistinguishable from converged ones, and convergence, when achieved, occurs early\.

![Refer to caption](https://arxiv.org/html/2606.06656v1/x5.png)Figure 5:Costas\-10 \(≈\\approx10% assigned\): We show the same view for this problem as in Figure[4](https://arxiv.org/html/2606.06656#S3.F4)This difference has important implications\. In vectorised CLS, all batch elements must iterate together; idling converged elements waste compute\. The convergence profile directly determines the cost of the maximum\-steps hyperparameter\. For unimodal profiles, setting the limit near the distribution’s central mass minimises waste\. For bimodal profiles, this becomes a throughput\-quality trade\-off: a lower limit improves throughput but terminates unconverged descents, while a higher limit wastes cycles on already\-converged elements\.

Note that Kyrillidis et al\.\[kyrillidis2021solving\]prove a polynomial upper bound on the number of PGD steps for convergence of orderO\(\|\#vars∥\#constraints\|\)O\(\|\\text\{\\\#vars\}\\parallel\\text\{\\\#constraints\}\|\), which greatly exceeds the empirically observed step counts\. Furthermore, this bound assumes algebraic precision, which cannot be maintained on accelerator hardware with limited floating\-point precision\.

## 4Related Work

The CLS approach builds on the Fourier analysis of Boolean functions\[odonnell14\]and its application to SAT\[kyrillidis2021solving\]\. GPU\-accelerated evaluation via DFT was introduced by Cen et al\.\[cen2025massively\]\. The representational advantages of PB constraints over CNF have been studied extensively\[sinz2005towards,bailleux2003efficient,warners1998linear,10\.1007/978\-3\-031\-95973\-8\_8\], with proof\-complexity results showing that resolution \(and CDCL\) can struggle with PB constraints in CNF\[10\.1145/7531\.8928,COOK198725,10\.1007/978\-3\-319\-94144\-8\_18,10\.1007/978\-3\-319\-94144\-8\_5\]\. State\-of\-the\-art PB solvers such asSCIP\[10\.5555/3215359\.3215361,BolusaniEtal2024OO\]use mixed\-integer programming techniques but remain inherently sequential\. Parallel SAT solving has been studied extensively\[DBLP:journals/aim/HamadiW13,katsirelos:2013\], but GPU\-based approaches remain non\-competitive with state\-of\-the\-art sequential systems\. The CLS approach builds on the Fourier analysis of Boolean functions\[odonnell14\]and its application to SAT\[kyrillidis2021solving\]\. GPU\-accelerated evaluation via DFT was introduced by Cen et al\.\[cen2025massively\]\. The representational advantages of PB constraints over CNF have been studied extensively\[sinz2005towards,bailleux2003efficient,warners1998linear,10\.1007/978\-3\-031\-95973\-8\_8\], with proof\-complexity results showing that resolution \(and CDCL\) can struggle with PB constraints in CNF\[10\.1145/7531\.8928,COOK198725,10\.1007/978\-3\-319\-94144\-8\_18,10\.1007/978\-3\-319\-94144\-8\_5\]\. State\-of\-the\-art PB solvers such asSCIP\[10\.5555/3215359\.3215361,BolusaniEtal2024OO\]use mixed\-integer programming techniques but remain inherently sequential\. Parallel SAT solving has been studied extensively\[DBLP:journals/aim/HamadiW13,katsirelos:2013\], but GPU\-based approaches remain non\-competitive with state\-of\-the\-art sequential systems\.

## 5Conclusions and Future Work

We studied continuous local search in GPU accelerated computing environments\. We catalogued a family of symmetric pseudo\-Boolean constraints that offer a representational advantage over CNF\. In our setting the compactness of pseudo\-Boolean problem representation enables a higher number of parallel local searches\. Our empirical evaluation has revealed several novel phenomena:

- •Problems that are expressed with redundant constraints cause search to exhibit gradient imbalances that inhibit convergence, suggesting that minimal PB encodings are preferable for CLS\.
- •CLS can reliably complete partial assignments for hard random33\-SAT with1515–20%20\\%of variables fixed, with monotonically improving performance as more variables are fixed, thus has potential for use as a sub\-solver\.
- •Convergence profiles exhibit characteristic distributional shapes that depend on problem structure and the fraction of free variables, with direct implications for parameter selection\.

Future work will pursue:\(i\)principled adaptive weighting schemes for heterogeneous PB problems, informed by per\-constraint gradient magnitude analysis;\(ii\)integration of CLS into distributed search architectures as exemplified byDagster;\(iii\)automated identification of PB substructures in CNF formulae and thereby compilation of CNF problems to compact representation amenable to CLS; and\(iv\)investigation of CLS for discovering problem constitutionality and dependency structures\.

## References

## Appendix AClosed\-Form Fourier Coefficients for Symmetric PB Constraints

We present closed\-form solutions for the Fourier coefficients of all symmetric PB constraint types supported by CLS\. In each case,SSdenotes a subset of variables, with\|S\|\|S\|substitutable forSSdue to symmetry, andnnis the total number of variables\.

Disjunction \(OR\):

OR^​\(S\)=\{12n−1−1\|S\|=012n−1\|S\|≠0\\displaystyle\\widehat\{\\texttt\{OR\}\}\(S\)=\\begin\{dcases\}\\frac\{1\}\{2^\{n\-1\}\}\-1&\\left\\lvert S\\right\\rvert=0\\\\ \\frac\{1\}\{2^\{n\-1\}\}&\\left\\lvert S\\right\\rvert\\neq 0\\end\{dcases\}
Exactly\-One \(EO\):

EO^​\(S\)=\{1−n2n−1\|S\|=02​\|S\|−n2n−1\|S\|≠0\\displaystyle\\widehat\{\\texttt\{EO\}\}\(S\)=\\begin\{dcases\}1\-\\frac\{n\}\{2^\{n\-1\}\}&\\left\\lvert S\\right\\rvert=0\\\\ \\frac\{2\\left\\lvert S\\right\\rvert\-n\}\{2^\{n\-1\}\}&\\left\\lvert S\\right\\rvert\\neq 0\\end\{dcases\}
Exactly\-kk\(EK\):

Ek^​\(S\)\\displaystyle\\widehat\{\{\\texttt\{E\}\_\{k\}\}\}\(S\)=\{1−\(nk\)2n−1\|S\|=0gEK​\(ρ\)\[ρ\|S⊢1\]​\(n−1\|S⊢1\)​2n−1\|S\|≠0\\displaystyle=\\begin\{dcases\}1\-\\frac\{\\binom\{n\}\{k\}\}\{2^\{n\-1\}\}&\\left\\lvert S\\right\\rvert=0\\\\ \\frac\{g\_\{\\texttt\{EK\}\}\(\\rho\)\_\{\[\\rho^\{\|S\\vdash 1\}\]\}\}\{\}\{\\binom\{n\-1\}\{\|S\\vdash 1\}2^\{n\-1\}\}&\\left\\lvert S\\right\\rvert\\neq 0\\end\{dcases\}gEK​\(ρ\)\\displaystyle g\_\{\\texttt\{EK\}\}\(\\rho\)=\(\(2​k−n\)\+n​ρ\)k​\(n−1k−1\)​\(1\+ρ\)n−k−1​\(1−p\)k−1\\displaystyle=\\frac\{\(\(2k\-n\)\+n\\rho\)\}\{k\}\\binom\{n\-1\}\{k\-1\}\(1\+\\rho\)^\{n\-k\-1\}\(1\-p\)^\{k\-1\}=1n​\(nk\)​\(\(2​k−n\)\+n​ρ\)​\(1\+ρ\)n−k−1​\(1−p\)k−1\\displaystyle=\\frac\{1\}\{n\}\\binom\{n\}\{k\}\(\(2k\-n\)\+n\\rho\)\(1\+\\rho\)^\{n\-k\-1\}\(1\-p\)^\{k\-1\}
At\-Most\-One \(AMO\):

AMO^​\(S\)=\{1−n−12n−1\|S\|=02​\|S\|−n−12n−1\|S\|≠0\\displaystyle\\widehat\{\\texttt\{AMO\}\}\(S\)=\\begin\{dcases\}1\-\\frac\{n\-1\}\{2^\{n\-1\}\}&\\left\\lvert S\\right\\rvert=0\\\\ \\frac\{2\\left\\lvert S\\right\\rvert\-n\-1\}\{2^\{n\-1\}\}&\\left\\lvert S\\right\\rvert\\neq 0\\end\{dcases\}
Not\-All\-Equal \(NAE\): The spectrums​pNAE=\{1,−1,−1,…,−1,1\}sp\_\{\\texttt\{NAE\}\}=\\left\\\{1,\-1,\-1,\\ldots,\-1,1\\right\\\}simplifies the noise operator tog​\(ρ\)=\(1\+ρ\)n−1−\(1−ρ\)n−1g\(\\rho\)=\(1\+\\rho\)^\{n\-1\}\-\(1\-\\rho\)^\{n\-1\}\. By the binomial theorem, even\-order terms cancel:

NAE^​\(S\)=\{12n−2−1\|S\|=012n−2\|S\|even0\|S\|odd\\displaystyle\\widehat\{\\texttt\{NAE\}\}\(S\)=\\begin\{dcases\}\\frac\{1\}\{2^\{n\-2\}\}\-1&\\left\\lvert S\\right\\rvert=0\\\\ \\frac\{1\}\{2^\{n\-2\}\}&\\left\\lvert S\\right\\rvert\\ \\ \\text\{even\}\\\\ 0&\\left\\lvert S\\right\\rvert\\ \\ \\text\{odd\}\\end\{dcases\}
Exclusive\-Or \(XOR\): The alternating spectrums​pXOR=\{1,−1,1,−1,…\}sp\_\{\\texttt\{XOR\}\}=\\left\\\{1,\-1,1,\-1,\\ldots\\right\\\}produces total cancellation of all terms ing​\(ρ\)g\(\\rho\)except2n−1​ρn−12^\{n\-1\}\\rho^\{n\-1\}\. ThusXORhas a single non\-zero coefficient:

XOR^​\(S\)=\{0\|S\|≠\[n\]1\|S\|=\[n\]\\displaystyle\\widehat\{\\texttt\{XOR\}\}\(S\)=\\begin\{dcases\}0&\\left\\lvert S\\right\\rvert\\neq\[n\]\\\\ 1&\\left\\lvert S\\right\\rvert=\[n\]\\end\{dcases\}
Cardinality\-kk\(CARD\):

CARD^≥k​\(S\)=\{1−∑i=kn\(ni\)2n−1\|S\|=0\(n−1k−1\)​\(gCARD​\(ρ\)\)\[ρ\|S\|−1\]\(n−1\|S\|−1\)​2n−1\|S\|≠0\\displaystyle\\widehat\{\{\\texttt\{CARD\}\}\}\_\{\\geq k\}\(S\)=\\begin\{dcases\}1\-\\frac\{\\sum\_\{i=k\}^\{n\}\\binom\{n\}\{i\}\}\{2^\{n\-1\}\}&\\left\\lvert S\\right\\rvert=0\\\\ \\frac\{\\binom\{n\-1\}\{k\-1\}\\left\(g\_\{\\texttt\{CARD\}\}\(\\rho\)\\right\)\_\{\[\\rho^\{\\left\\lvert S\\right\\rvert\-1\}\]\}\}\{\\binom\{n\-1\}\{\\left\\lvert S\\right\\rvert\-1\}2^\{n\-1\}\}&\\left\\lvert S\\right\\rvert\\neq 0\\end\{dcases\}gCARD​\(ρ\)=\(1\+ρ\)n−k​\(1−ρ\)k−1\\displaystyle g\_\{\\texttt\{CARD\}\}\(\\rho\)=\(1\+\\rho\)^\{n\-k\}\(1\-\\rho\)^\{k\-1\}
These closed\-form solutions enable polynomial\-time coefficient computation for all constraint types, providing the foundation for CLS on heterogeneous PB problems\.

## Appendix BCNF Encoding Tables

Clause Typeϕ\\phiPB FormFEϕ\\texttt\{FE\}\_\{\\phi\}/O​\(f^​\(S\)\)O\(\\hat\{f\}\(S\)\)O​\(\#​CNF​\(f\)\)O\(\\\#\\texttt\{CNF\}\(f\)\)Disjunction \(OR\)∑nxn≥1\\sum\_\{n\}x\_\{n\}\\geq 1O​\(1\)O\(1\)—At most one \(AMO\)∑nxn≤1\\sum\_\{n\}x\_\{n\}\\leq 1O​\(n\)O\(n\)NaïveO​\(n2\)O\(n^\{2\}\),O​\(log⁡n\)O\(\\log n\)Exactly one \(EO\)∑nxn=1\\sum\_\{n\}x\_\{n\}=1O​\(n\)O\(n\)NaïveO​\(n2\)O\(n^\{2\}\),O​\(log⁡n\)O\(\\log n\)Exactlykk\(EK\)∑nxn=k\\sum\_\{n\}x\_\{n\}=kO​\(n​log2⁡n\)O\(n\\log^\{2\}\{n\}\)See Table[3](https://arxiv.org/html/2606.06656#A2.T3)\.Not all equal \(NAE\)⋀\{∑nxn<n∑nxn\>0\\bigwedge\\begin\{cases\}\\textstyle\\sum\_\{n\}x\_\{n\}<n\\\\ \\textstyle\\sum\_\{n\}x\_\{n\}\>0\\end\{cases\}O​\(1\)O\(1\)O​\(1\)O\(1\)Exclusive Or \(XOR\)∑nxn≡1\(mod2\)\\sum\_\{n\}x\_\{n\}\\equiv 1\\pmod\{2\}O​\(n\)O\(n\)O​\(n\)O\(n\)Cardinality\-kk\(CARD\)∑nxn≥k\\sum\_\{n\}x\_\{n\}\\geq kO​\(n​log2⁡n\)O\(n\\log^\{2\}\{n\}\)See Table[3](https://arxiv.org/html/2606.06656#A2.T3)\.

Table 2:Asymptotic costs of Fourier coefficient computation vs\. CNF translation for symmetric PB constraints\.Encoding\#\\\#clauses\#\\\#aux\. varsNaïve\(nk\+1\)\\binom\{n\}\{k\+1\}0Sequential unary counterO​\(n⋅k\)O\(n\\cdot k\)O​\(n⋅k\)O\(n\\cdot k\)Parallel binary counter7​n−3​⌊log⁡n⌋−67n\-3\\lfloor\\log n\\rfloor\-62​n−22n\-2Bailleux and Boufkhad\[bailleux2003efficient\]O​\(n2\)O\(n^\{2\}\)O​\(n⋅log⁡n\)O\(n\\cdot\\log n\)Warners\[warners1998linear\]8​n8n2​n2nTable 3:CNF encodings for Cardinality\-kk\[sinz2005towards\]\. All non\-naïve encodings introduce auxiliary variables\.