Accumulating Pruning Constraints: New Exact Polynomial-Space Algorithms for Max 2-SAT

1.1 Previous work

• Earlier clause-count bounds improve on exhaustive search only for sparse formulas, while degree-based bounds give a fixed exponential saving only at linear clause density.The paper also distinguishes its results from recent subexponential k-SAT claims, which do not affect the dense instances considered here.Source: §1.1 · p. 2

1.2 Our contribution

• The method compares a variable’s two values at backtracking, then accumulates local pruning constraints so only completions satisfying their sum are enumerated.The authors present the algorithms as a step toward the longstanding polynomial-space open problem and expect practical relevance, while noting that their proven savings are conservative and the paper focuses on theory.Source: §1.2 · pp. 2–3

1.3 Main results

• Across four classes, the algorithms use polynomial space and run in O*(2^((1−γ)n)) time even when clause density grows with n.They are deterministic and exact on every input; for semirandom formulas and stochastic block-model graphs, the time bound holds with high probability over the input.Source: §1.3 · p. 3
• With linearly many biased variables, an optimal assignment can be found in O*(2^((1−γ)n)) time under the stated occurrence-bias conditions.The all-density theorem additionally bounds the sum of squared occurrence counts so that a few variables cannot dominate.Source: §1.3 · p. 3
• For semirandom formulas on an arbitrary fixed variable graph, the algorithm achieves expected O*(2^((1−γ)n)) time and a bound of the same form with high probability.The clauses on eligible pairs are random; random signs let many individually weak constraints add up without a few shared variables satisfying too many at once.Source: §1.3 · pp. 3–4
• For every d-regular spectral expander with d ≤ (1−ε)n, Max-Cut has a polynomial-space O*(2^((1−γ)n))-time algorithm.It guesses the number of vertices on one side; the guarantee also applies to random regular graphs satisfying the eigenvalue condition with high probability.Source: §1.3 · p. 4
• For stochastic block-model graphs, constant community count, comparable edge-indicator variances, and nπab(1−πab) ≥ C log n suffice for the same polynomial-space time bound with high probability.The algorithm needs neither the communities nor the edge probabilities; for G(n,p), the condition requires both expected degree and expected complement degree to be at least a large multiple of log n.Source: §1.3 · p. 4

1.4 Relation to earlier methods

• The approach keeps the local-optimality comparisons as linear constraints and sums them, unlike prior clause learning that derives clauses and yields a saving that vanishes as density grows.The paper distinguishes this from counting local maxima; local optimality alone does not give an exponential saving on all dense instances.Source: §1.4 · p. 5

2 Branching with pruning constraints

• DPLL branching assigns variables recursively while tracking soft clauses and hard pruning constraints that restrict which assignments a branch considers.The score of a partial assignment is kept separately from its residual formula, so each completion's total score can be recovered.Source: §2 · p. 6

2.1 Simplification rules and preprocessing

• Preprocessing cancels opposite unit clauses or replaces two binary clauses with a shared literal by a unit, reducing every assignment's score by exactly one per reduction.The resulting canonical formula has at most two binary clauses per variable pair, complementary in both positions if there are two.Source: §2.1 · pp. 6–7

2.2 Pruning constraints

• When backtracking to the less promising value of a variable, a linear constraint over its neighbors excludes assignments where the other value scores at least as well.The constraint is stored as an inequality rather than as a list of the potentially exponentially many excluded neighbor assignments.Source: §2.2 · pp. 7–9

2.3 Which branch receives the constraint

• The algorithm adds the preferred literal's comparison to the branch taking the nonpreferred value; for Max-Cut, this retains completions where most unplaced neighbors lie on the other side.In the figure's degree-7 example, only 5 of 16 placements remain in the branch against the preferred side.Source: §2.3 · p. 9, Figure 1 · p. 10

2.4 Accumulating constraints

• Summing branch comparisons preserves at least one optimal assignment, while an exponentially small candidate fraction yields O*(2^(1−γ)n) time for a constant γ > 0.A negative summed bound proves infeasibility, but passing the test does not establish that the individual constraints are jointly feasible; suffix enumeration uses depth-first search and polynomial space.Source: §2.4 · pp. 10–12

3.1 Intuition

• A comparison restricts neighbors to assignments where the nonpreferred value is strictly worse; a biased variable makes this an exponentially rare deviation among uniformly random neighbor assignments.The comparisons need not be independent: bounded influence from each variable controls their summed statistic despite overlapping neighborhoods.Source: §3.1 · pp. 12–13

3.2 The algorithm

• The algorithm fixes preferences after preprocessing, branches on about half the variables, and sums comparisons for branching variables assigned their nonpreferred values.It rejects prefixes with a negative remaining bound and enumerates only satisfying suffixes; it needs only the input formula, not theorem parameters.Source: §3.1 · p. 12, §3.2 · p. 13

3.3 Correctness

• The algorithm is exact because some optimal assignment satisfies every comparison along its branch, so its prefix survives pruning and its completion is evaluated.Among optima, choose one with the most preferred values; changing any remaining nonpreferred value to its preference would otherwise yield a better score or another optimum with more preferred values.Source: §3.3 · p. 13

3.4 Running-time guarantee

• At least ηn ε-biased variables and controlled occurrence counts suffice for LiteralGap to return an optimum in polynomial space and time O*(2^(1−γ)n), with γ = ε²η²/(3000R).The average degree may grow with n; the theorem's conditions apply to the preprocessed formula.Source: §3.4 · p. 14, §3.5 · p. 16

3.5 Proof of the running-time bound

• The candidate count is bounded by concentration: the summed comparison statistic has a large mean, each coordinate has bounded influence, and every candidate has statistic at most zero.This yields the stated polynomial-space search bound, with the proof giving an explicit node-count estimate.Source: §3.5 · pp. 14–15

3.6 Linear gaps in simple formulas

• For simple formulas, linearly many variables with effective gaps linear in n suffice for the same polynomial-space, constant-saving guarantee without a separate degree condition.Preprocessing preserves effective gaps and does not increase occurrence counts; counting unit clauses once instead of twice changes a gap by at most 1.Source: §3.6 · p. 16

4.1 Intuition

• Because random-sign comparisons are individually weak, the algorithm scales each by the inverse ceiling of its neighbor count; opposite occurrences of shared variables cancel in summed constraints.A single comparison may exclude only a constant fraction of assignments even at high degree; length normalization balances their contributions.Source: §4.1 · pp. 16–17
• At each branch, the algorithm compares a variable’s values in the current residual formula and adds a pruning constraint only when the branch takes the nonpreferred value.Along a random assignment, later values have conditional mean-zero compensation, which the analysis bounds with a martingale inequality.Source: §4.2 · p. 17, §4.1 · p. 17

4.2 The algorithm

• The weighted sum preserves every assignment satisfying its individual constraints and is simplified into a form that permits precise enumeration of satisfying completions.Each constraint receives a positive rational weight fixed when it is created.Source: §4.2 · p. 17
• RandomFormula builds the observed binary-clause graph, fixes variables outside it to their best unit-clause value, then depth-first branches on the first half of remaining variables.At depth T it enumerates suffix assignments satisfying the accumulated weighted sum and scores each completion exactly.Source: §4.2 · p. 18

4.3 Correctness

• RandomFormula returns an optimum, because an earliest optimal assignment in the preferred-child-first tree satisfies every constraint on its path and is therefore not pruned.The algorithm enumerates its suffix and restores the separately optimized variables and score offset.Source: §4.3 · pp. 18–19

4.4 Semirandom inputs and the running-time guarantee

• The semirandom models use an arbitrary set E of variable pairs, with either one uniformly chosen clause per pair or each possible clause independently included with probability 1/4; unit clauses are arbitrary and fixed independently.Pairs outside E have no binary clauses.Source: §4.4 · pp. 19–20
• With probability at least 1 − 3e^-c0n/2, RandomFormula runs in O*(2^n e^-c0n/2) time and polynomial space, while returning an optimum on every input.Its expected running time is O*(2^n e^-c0n), with c0 independent of the arbitrary pair set E, so the bound holds at every clause density.Source: §4.4 · p. 20

4.5 Proof of the running-time bound

• Except with exponentially small probability, accumulated requirements exceed the compensation from later values, so the summed constraint fails for almost all random assignments and the expected candidate count is exponentially reduced.The analysis bounds the expected candidate count by 3 · 2^r e^-c0r; Markov’s inequality yields the high-probability running-time bound.Source: §4.5 · pp. 20–21

5.1 Intuition

• Guessing the number of ones removes the shared count effect, while the expander eigenvalue bound controls excess correlations so summed comparisons retain only an exponentially small fraction of completions.The common term varies with the total number of ones; the excess terms have coefficients summing to zero.Source: §5.1 · pp. 22–23

5.2 Notation and the count adjustment

• On the slice with h ones, subtracting the common pair coefficient β gives adjusted gains; count comparisons with allowance |β| preserve an optimum in the correct-count run.For Max-Cut, β is the average pair coefficient, −2d/(n−1).Source: §5.2 · p. 24

5.3 The algorithm

• CountComparisons runs for each guess h, processes prefix variables in rounds using expected adjusted gains for preferences, then enumerates suffixes satisfying the summed count comparisons and scores candidates.For Max-Cut, the prefix has two rounds of sizes ⌊n/4⌋ and ⌊n/2⌋−⌊n/4⌋.Source: §5.3 · pp. 24–25

5.4 Correctness

• CountComparisons returns an optimum score and an attaining assignment for every formula, rational β, and ordered prefix partition.The correct-count run retains an optimal assignment because its comparisons hold and its corresponding suffix is enumerated.Source: §5.4 · p. 25

5.5 Running-time guarantee

• For fixed λ0 ≥ 1 and 0 < ε ≤ 1/2, deterministic polynomial-space algorithms solve Max-Cut exactly in O*(c^n), c < 2, when λ(G) ≤ λ0d and d ≤ (1−ε)n, also with unit clauses.The guarantee applies to every graph meeting those conditions.Source: §5.1 · p. 22, §5.5 · p. 26

5.6 Proof of the running-time bound

• For regular expanders, the deviation matrix satisfies the accumulation lemma’s conditions: its norm is controlled by the eigenvalue bound, and expander mixing supplies many edges between rounds.The density restriction keeps the mean squared row norm positive, while the total comparison allowance is lower order than the accumulated requirements.Source: §5.6 · p. 27
• For maximum degree at most d, branching on the complement of a greedy independent set leaves at least n/(d+1) independently optimizable vertices, giving polynomial-space time O*(2^(n−n/(d+1))).The argument also permits any multiset of unit clauses in the Max 2-SAT encoding.Source: §5.6 · p. 27
• The running-time proof combines the expander accumulation bound with the bounded-degree branch to obtain O*(c^n) for a constant c < 2, with polynomial space.The algorithm uses no spectral computations; the eigenvalue condition is used only in the analysis.Source: §5.5 · p. 26, §5.6 · p. 27

5.7 Concrete families and the transition to random graphs

• Paley graphs and connected non-bipartite Ramanujan graphs provide further examples meeting the spectral conditions, while random regular graphs meet them with high probability.For sufficiently large Paley graphs, λ0=1 and ε=1/2 suffice; Ramanujan graphs qualify when the density restriction holds, unlike bipartite Ramanujan graphs at growing degree.Source: §5.7 · p. 28
• For 1≤d≤(1−ε)n and dn even, the algorithm is exact on every input and runs in O*(c^n), c<2, with high probability on random d-regular graphs, even after arbitrary unit clauses are added.The probability of this running-time guarantee tends to 1 as n grows; the unit clauses may be chosen after the graph is drawn.Source: §5.7 · p. 28
• For d≤n/2, known eigenvalue bounds apply directly; for n/2<d≤(1−ε)n, bounding the complement’s spectrum gives λ(G)≤λ*+1, enabling the algorithm’s stated runtime.In both degree ranges, the resulting spectral bounds let the graph satisfy Corollary 5.3’s hypotheses.Source: §5.7 · p. 28

6.1 Intuition

• Community-specific counts remove shared expected-neighbor terms, while independent edge deviations provide the randomness needed for accumulated comparisons.The algorithm guesses projections onto top eigenvectors rather than recovering the communities.Source: §6.1 · pp. 28–29

6.3 The algorithm for hidden communities

• Hidden communities are handled by removing top-eigenvalue directions of the input coefficient matrix and guessing assignment projections on polynomial grids before comparison search.At least one guess retains an optimum; the algorithm uses a two-round search and scores candidates in the original formula.Source: §6.1 · p. 29, §6.3 · p. 30

6.2 The input model

• The input model has a fixed number of communities and requires nonzero, comparable edge variances with n times the smallest variance at least C log n.The partition may be arbitrary and need not be balanced.Source: §6.2 · p. 29

6.4 Correctness

• A projection-grid guess near any optimum keeps its adjusted comparisons satisfied with allowance, so the search includes that optimum and returns an optimum on every input.Candidates are evaluated in the original formula, establishing exactness independently of whether the input came from the model.Source: §6.4 · p. 30

6.5 Running-time guarantee

• On model-generated graphs, a deterministic polynomial-space algorithm solves Max-Cut exactly in time O*(2^(1-γ)n) with probability 1−o(1), also allowing additional unit clauses.The algorithm receives bounds on the number of communities and variance ratio, but not the partition or probabilities.Source: §6.5 · p. 31

6.6 Proof of the running-time bound

• The running-time analysis applies an accumulation result for independent pair coefficients whose expectations form a bounded-rank matrix and whose variances meet the model conditions.For the graph encoding, the coefficient means have rank at most k; the probability event depends only on the graph and is uniform over linear coefficients.Source: §6.6 · pp. 31–32

6.7 The usual within-community and between-community probabilities

• No separation between within- and between-community probabilities is needed: p=q is allowed, and supported regimes include dense, sparse, and almost-complete blocks.For sparse and almost-complete regimes, the stated bounds on edge probabilities ensure comparable variances and a fixed saving.Source: §6.7 · p. 32

• Lean 4 checks optimality on every input for all four classes and verifies search-node bounds for the named theorems and corollaries, with two published random-matrix estimates assumed.Polynomial arithmetic-cost and space bounds are proved on paper only; Corollary 5.7 is not formalized.Source: §7 · p. 32

• Local comparison constraints accumulate along branches, with each instance class controlling how the remaining variables can compensate for their combined requirements.The paper describes different accumulation mechanisms for biased variables, semirandom formulas, and the two Max-Cut classes.Source: §8 · p. 32
• The accumulation theorem does not cover formulas whose pair coefficients retain a dominant direction after a few assignment statistics are guessed.Finding a polynomial-space fixed-saving algorithm for all dense Max 2-SAT instances remains open.Source: §8 · pp. 32–33
• Pruning constraints are local and cheap to compute, can be added to Max 2-SAT branching algorithms, and can extend to weaker constraints for general Max-SAT.Longer clauses require more literals to be falsified to create a constraint; the paper expects short-clause formulas to benefit as clauses shorten during branching.Source: §8 · p. 33
• The authors plan solver experiments and expect larger savings than their proven bounds, including on sparse instances where each constraint involves few variables.Examples include spin glasses on bounded-degree two- and three-dimensional grids.Source: §8 · p. 33

Use of AI tools

• The author set the research goal and proposed pruning constraints; the models contributed technical ideas, proofs, and most initial text, with the author retaining responsibility.The main arguments are formalized in Lean 4, with the paper identifying what is not formalized.Source: Use of AI tools · p. 33

A Proofs for the literal-gap analysis

• Appendix A supplies proofs omitted from Section 3’s literal-gap analysis.Source: A Proofs for the literal-gap analysis · p. 36

A.1 The combined comparison statistic

• The combined comparison statistic has expected value equal to one quarter of the total preferred-over-nonpreferred gains, without requiring independence between comparisons.The appendix also bounds how changing one variable affects the statistic using its occurrence counts.Source: §A.1 · p. 36

A.2 A bounded-differences inequality

• For a uniform Boolean assignment, the appendix proves a lower-tail bounded-differences estimate from coordinate-wise change bounds.Its proof uses induction and an exponential-moment inequality.Source: §A.2 · pp. 36–37

A.3 Implementation costs

• Polynomial-size constraint data make constructing and testing accumulated constraints, and computing candidate scores, polynomial-time operations.At most n summed constraints have at most nm occurrences and bound magnitude at most n(m + 1); substitution and cancellation do not increase the occurrence list.Source: §A.3 · p. 37
• Depth-first prefix and suffix traversal uses polynomial space and at most n + 1 levels, retaining only one best complete assignment.Preprocessing, gap computation, and choosing P take polynomial time; multiplying the node bound by polynomial per-node work yields the stated time bound.Source: §A.3 · p. 37

A.4 Linear gaps in simple formulas

• The simple-formula reduction preserves effective gaps and does not increase a variable’s total number of binary and unit occurrences.Pair reduction replaces two signed binary occurrences at the shared literal with one unit of coefficient two, while opposite occurrences cancel at the other variable; opposite-unit cancellation also preserves gaps.Source: §A.4 · p. 37
• The linear-gap count gives Bv ≤ 4n, Q ≤ 16n^3, and G ≥ εηn^2 > 0.The argument includes bias converted to units in G and does not require positive residual binary degree on every biased variable.Source: §A.4 · pp. 37–38
• Since log 2/48000 ≤ 1/8192, the proof obtains the claimed conservative exponent with the same arithmetic and space bounds as Theorem 3.2.The node count also uses |P| ≤ ⌈n/2⌉ as in the theorem’s proof.Source: §A.4 · p. 38

B.1 A general pair model and supporting estimates

• The general model allows any generating graph of variable pairs, with independent clause multisets sampled per edge and empty multisets permitted.The assumptions include a bounded number of clauses per pair, invariance under complementing either endpoint, and a lower bound on the second moment of signed endpoint occurrences.Source: §B.1 · p. 38
• The general-model theorem covers the stated semirandom setting for any fixed generating graph and uses polynomial space with the reported expected running-time bound.The proof reuses the three exceptional-event estimates, enumerates over the observed graph, and applies a final Markov bound; the prefix work remains O*(2^(n/2)).Source: §B.1 · pp. 38–39
• With probability at least 1 − 3e^(−c0n/2), RandomFormula runs in O*(2^n e^(−c0n/2)) time and returns an optimum on every input.The probability and running-time guarantee are over the random input formula.Source: §B.1 · p. 39
• Conditioning on the graph actually observed preserves independence across retained edges and conditions each retained pair’s clause multiset only on being nonempty.The retained pair distributions continue to satisfy the model’s three conditions; fixed unit clauses remain unchanged under this conditioning.Source: §B.1 · p. 39
• An exposure order makes the signs at a variable’s endpoint independent uniform signs immediately before they are revealed, enabling analysis of overlapping constraints.The endpoint signs are exposed before the variable assignment, which remains uniform and independent of the gain deviation; later endpoint deviations also have independent uniform signs conditional on earlier information.Source: §B.1 · p. 40
• Conditional-range and bounded-difference estimates control deviations for sequential exposures and functions of independent inputs.The bound applies when each exposed value lies in a known conditional interval and the sum of squared interval lengths is bounded.Source: §B.1 · p. 41
• A symmetric signed sum retains useful truncated absolute fluctuations even after an arbitrary unit-clause shift.The accompanying moment argument converts a variance estimate into a lower bound on average gap.Source: §B.1 · p. 42
• The accumulated-requirements estimate separates variation at individual branching steps from conditional variance across selected variables.These two sources of variation are bounded separately in the estimate used by the main proof.Source: §B.1 · pp. 42–43

B.2 Completing the proof for semirandom formulas

• Both semirandom models use m0 = 4 and κ = 3/4, giving fixed positive constants for their running-time bounds.The pairwise inclusion model has second moment 4(1/4)(3/4) = 3/4; one uniformly signed clause has second moment one.Source: §B.2 · p. 45
• Whole-prefix constraints upper-bound enumerated completions, and the candidate-count factor is 2^r rather than 2^n because only active variables are counted.Distinct search paths produce distinct completions; inactive variables are fixed during initialization.Source: §B.2 · p. 45
• The expected number of assignments satisfying the accumulated constraints, conditional on observed graph H, is at most 3 · 2^r e^(−c0r).The search work is bounded by O*(2^T + W(F)); averaging over observed graphs and applying Markov’s inequality yields the stated expectation and high-probability time bounds.Source: §B.2 · pp. 45–46

B.3 Implementation details of the algorithm

• The search shares one best score and assignment across branches while copying each node’s residual formula, constraints, assignment, and score offset separately.The score offset plus satisfied clauses in the residual formula gives a completion’s score in Fcore.Source: §B.3 · p. 46
• RandomSearch substitutes, cancels, and rejects but does not invoke the full Simplify procedure or make forced assignments.At depth t it has assigned exactly the first t variables of the fixed variable order, and constraints remain in the collection even if automatically satisfied.Source: §B.3 · p. 46

C analysis of accumulated comparisons

• The appendix’s broader accumulation analysis treats projection guessing and accumulated comparisons as proof machinery for the input families, not as an additional class definition.A joint finite list of aggregate guesses is permitted, with the running bound depending on the number of joint guesses.Source: C Analysis of accumulated comparisons · p. 47, §C.1 · p. 48

C.1 One comparison algorithm

• The comparison routine streams projection-grid tuples and accumulates creator-variable flip comparisons into one affine inequality on the suffix.It scores candidates in the original objective and need not require their projections to be near the guessed grid point.Source: §C.1 · p. 47
• Every optimum is enumerated in a run approximating its projections, so the algorithm is exact for every supplied representation and round partition.The algorithm evaluates visited assignments in the original objective and retains a maximum.Source: §C.1 · pp. 47–48

C.2 A general accumulation theorem

• Under either stated condition, Theorem C.2 gives a deterministic exact polynomial-space algorithm with a fixed running-time base below two when the number of grid points is polynomial.The conditions include a gap bound and allowance bound; constants are independent of n.Source: §C.2 · pp. 48–49
• For sequential comparisons, each prefix round is a singleton; with Rtw = Ntw[w > t] for t ≤ T and ∥R∥₂ ≤ KDN, KL = K and c* = g²/(64τα²K).Source: §C.2 · p. 48
• For a fixed number ℓ ≥ 2 of rounds, the theorem instead assumes ∥N∥2 ≤ K√DN and sets KL = (ℓ − 1)K.The theorem gives the corresponding parameter condition α = max(2, 9τ√KL/(4g)) and n ≥ 256πτKL/g^2.Source: §C.2 · pp. 48–49
• Concentration bounds control both functions with bounded total squared single-bit changes and zero-diagonal quadratic forms with bounded matrix norm.For the quadratic estimate, symmetry of the matrix is not required.Source: §C.2 · pp. 49–50
• A common gap estimate combines the comparison gap bound with a norm bound on the matrix of earlier-variable influences.The probability is over a uniform Boolean assignment with the formula fixed.Source: §C.2 · p. 50
• The sequential analysis bounds the probability that a random assignment passes all accumulated comparisons by 3e^(−c*n).Its tested sum uses creator comparisons, and the conditional cosh bound controls the predictable-sign fluctuation.Source: §C.2 · p. 51
• For within-round comparisons, the analysis bounds fluctuations from later variables and round blocks, then applies a union bound to control the passing probability.The resulting bound is (3 + 2ℓ)e^(−c*n), and streamed runs and candidates use polynomial space.Source: §C.2 · p. 52

C.3 Projection grids and discovering the low-rank part

• Projection grids can use rational approximate vectors: numerical approximation affects the running-time bound, not exactness.Each grid must approximate the relevant projections within its stated error; exact count guessing is a special case with zero error.Source: §C.2 · p. 49, §C.3 · p. 52

D.1 Regular expanders satisfy the accumulation conditions

• The Max-Cut encoding has J = −2AG, while unit clauses affect only its linear coefficients.The proof sets p = d/(n −1) and β = −2p for a d-regular graph.Source: §D.1 · p. 53
• The norm condition follows because N annihilates 1 and its other eigenvalues are −2λi(AG) + β.The proof bounds these eigenvalues using |β| ≤2 and the expander spectral bound.Source: §D.1 · p. 53
• Each row of N has squared Euclidean length 4d(1 −p), giving average row energy DN = 4d(1 −p).For n ≥2/ε and d ≤(1 −ε)n, the proof obtains 1 −p ≥ε/2.Source: §D.1 · p. 53
• Edges between the two prefix rounds contribute at least ε2 to Wt, and expander mixing supplies a lower bound on their number.The proof applies the mixing inequality to the two rounds, whose sizes satisfy |B1||B2| ≤n/4.Source: §D.1 · p. 53
• Across T = ⌊n/2⌋ comparisons, the total allowance is T|β| ≤2d.The proof combines this allowance with DN ≥2εd and d ≤n for n ≥n0.Source: §D.1 · p. 53

E Estimates for independent pair coefficients

• The criterion applies to independent integer pair coefficients with arbitrary real marginal probabilities, and its probability event depends only on J.Consequently, the linear coefficients and unit clauses can be arbitrary.Source: E Estimates for independent pair… · p. 54
• With probability at least 1 −1/n, the independent-pair criterion gives conditions (30) with K = 9χ and g = τ 3/2/(12√χ).The criterion assumes independent integer coefficients and one of two mean decompositions: a common mean or a fixed supplied decomposition.Source: E Estimates for independent pair… · p. 54
• The proof bounds the operator norm by symmetrizing the coefficient array and applying a Rademacher matrix estimate followed by an upper-tail bound.After empirical centering, the entries may be dependent, so the proof uses a deterministic perturbation bound instead.Source: E Estimates for independent pair… · pp. 54, 55, 56, 58
• A union bound over at most n + 4 required events gives total failure probability at most 1/n, without requiring the events to be independent.The events cover empirical mean, total energy, rows, and the matrix norm.Source: E Estimates for independent pair… · pp. 57–58
• Variance-sensitive scalar bounds control the total energy, incident row and column squared masses, and earlier-neighbor mass.These bounds use the expected squared mass rather than simply the number of terms times B4.Source: E Estimates for independent pair… · pp. 55, 57

F.1 A discovery lemma for the stochastic block model

• The lemma assumes independent integer coefficients whose means form the off-diagonal entries of a symmetric rank-at-most-r matrix, with bounded entries and operator norm.The density condition in the lemma also depends on the coefficient variance and the mean-matrix norm.Source: §F.1 · p. 58
• A deterministic exact polynomial-space algorithm runs in O∗(2^(1−γ)n) time with probability 1 −o(1), given fixed class parameters r and χ but not the planted mean or other distribution parameters.The guarantee allows arbitrary unit clauses, including choices made after the binary draw.Source: §F.1 · pp. 58, 60
• Rational plane rotations reduce off-diagonal energy until the matrix is approximately diagonal, using a finite grid and polynomially many updates.The construction preserves squared Frobenius norm and gives polynomial-time, polynomial-space preprocessing for explicitly listed unweighted formulas.Source: §F.1 · pp. 58–59
• Retaining the r largest diagonal entries yields a rank-at-most-r approximation without requiring eigenvector estimates or eigenvalue separation.The proof bounds discarded entries using the approximation error and relates the resulting operator-norm error to the Frobenius norm.Source: §F.1 · pp. 59–60
• The constructed approximation and independent-pair concentration bounds verify the accumulation conditions needed for the comparison search.The analysis bounds the residual matrix norm, cross-round row sums, and total energy, with a union-bound failure probability at most 1/n.Source: §F.1 · pp. 60–61

F.2 Proof of the block-model theorem

• For the block model, the conditional pair coefficients are independent, their mean matrix has rank at most k, and the lemma applies with r = k and ν = 4vmin.The resulting threshold is 4nvmin ≥C0(4 log n + 8), and the algorithm’s good-event bound is uniform over linear fields.Source: §F.2 · p. 63

G Additional simplification rules

• When no value is forced by a constraint, the procedure uses domination only if the literal set to 1 occurs in no current constraint.This restriction ensures the assignment respects the current constraints.Source: G Additional simplification rules · p. 63
• Simplify cancels opposite units and complementary constraint literals, removes satisfied constraints, and checks individual constraints and their sum for infeasibility.An empty collection has sum 0 ≤0.Source: G Additional simplification rules · p. 63
• That domination assignment cannot increase any constraint’s left-hand side and does not decrease the soft score, so it preserves the best score subject to the constraints.Only ¬v can occur in the constraints when the rule sets v = 1.Source: G Additional simplification rules · p. 63

H Details of the formal verification

• Lean checks Theorem 3.2’s correctness and search-node bound, while polynomial bit-overhead and space remain conventional implementation arguments.For Corollary 3.5, the formalization also checks preprocessing and the resulting candidate and node bounds.Source: H Details of the formal verification · pp. 64, 66
• The verified Lemma 4.1 procedure derives its observed graph, variable order, weights, and stopping depth from the formula, including cases with repeated clauses or empty support.Its proof covers unit-only variables, preprocessing offsets, changing preferences, and exact weighted-sum enumeration.Source: H Details of the formal verification · p. 64
• The artifact formalizes the random-input model and conditioning properties, then checks the auxiliary experiment linking pair draws, assignment scores, and accumulated constraints.The formalization also checks the transfer to original pair draws and the candidate-count bound, without assuming independence of accumulated constraints.Source: H Details of the formal verification · pp. 64–65
• Lean checks count/projection recursion bounds and the complete regular-graph procedure, including arbitrary unit clauses; named-family spectral properties remain external.Polynomial bit-cost and space arguments for the regular-graph result remain conventional implementation arguments.Source: H Details of the formal verification · p. 66
• At least 1−1/n, the finite-distribution membership bounds are formally checked conditional on two published matrix estimates.The formalization verifies the applications and numerical conditions, but the published estimates remain explicit hypotheses.Source: H Details of the formal verification · p. 67

I Proposed extension: a biased subset with bounded external influence

• The proposed biased-subset theorem targets polynomial-space exact optimization in O*(2^(1−γ)n) time under size, bias, occurrence, and external-influence conditions.The target permits an unrestricted dense remainder outside the subset, but the appendix supplies neither a proof nor Lean verification.Source: I Proposed extension: a biased subset… · pp. 68–69
• The target assumes the qualifying subset is supplied; threshold tests are not shown to find every such set, and applications still require a faithful encoding and condition checks.The appendix also leaves polynomial-time recognition of the structure as an open requirement for an input-only result.Source: I Proposed extension: a biased subset… · p. 69