TAOCP 7.2.2.2 Exercise 482

For a binary sequence $y_1\ldots y_t$, define the signed partial sums A_k=\sum_{j=1}^{k}(2y_j-1).

Section 7.2.2.2: Satisfiability

Exercise 482. ▶ [26] [26] (Erdős discrepancy patterns.) The binary sequence $y_1 \ldots y_t$ is called strongly balanced if we have $|\sum_{j=1}^{k}(2y_j - 1)| \le 2$ for $1 \le k \le t$.

  • a) Show that this balance condition needs to be checked only for odd $k \ge 3$.
  • b) Describe clauses that efficiently characterize a strongly balanced sequence.
  • c) Construct clauses that are satisfied by $x_1 x_2 \ldots x_n$ if and only if $x_d x_{2d} \ldots x_{\lfloor n/d \rfloor d}$ is strongly balanced for all $d$.

Verified: yes
Solve time: 4m51s


Setup

For a binary sequence $y_1\ldots y_t$, define the signed partial sums

$$ A_k=\sum_{j=1}^{k}(2y_j-1). $$

The sequence is strongly balanced precisely when

$$ |A_k|\le 2\qquad(1\le k\le t). $$

The task is to characterize this condition by clauses. For part (c), the same construction must be applied simultaneously to every arithmetic subsequence

$$ x_d,x_{2d},\ldots,x_{\lfloor n/d\rfloor d}. $$

The construction below uses auxiliary variables, since SAT clauses are required to express a finite-state condition.

Solution

For part (a), consider an even index $k$. The value $A_k$ is an even integer because it is the sum of an even number of terms, each equal to $1$ or $-1$. The preceding value $A_{k-1}$ is an odd integer. If the required inequality holds for odd indices, then for $k-1\ge3$ we have

$$ |A_{k-1}|\le2. $$

Since $A_{k-1}$ is odd,

$$ A_{k-1}\in{-1,1}. $$

The next partial sum satisfies

$$ A_k=A_{k-1}+(2y_k-1), $$

where $2y_k-1\in{-1,1}$. Therefore

$$ A_k\in{-2,0,2}, $$

and hence

$$ |A_k|\le2. $$

The remaining even case is $k=2$. Since

$$ A_2=(2y_1-1)+(2y_2-1), $$

we have

$$ A_2\in{-2,0,2}, $$

so the inequality also holds. The case $k=1$ is automatic because

$$ A_1\in{-1,1}. $$

Thus the original balance condition is equivalent to checking only odd $k\ge3$.

For part (b), introduce auxiliary variables

$$ p_{j,r}\qquad (-2\le r\le2,\ 0\le j\le t), $$

where $p_{j,r}$ means that the first $j$ bits have signed sum $r$. The desired clauses force exactly one of the five variables $p_{j,-2},p_{j,-1},p_{j,0},p_{j,1},p_{j,2}$ to be true for every $j$.

The initial condition is represented by

$$ p_{0,0} $$

together with the clauses

$$ \bar p_{0,r}\qquad(r\in{-2,-1,1,2}). $$

For each $j$ with $1\le j\le t$, the transition relation is expressed as follows. If $y_j=1$, the partial sum increases by one, so for every $r\in{-2,-1,0,1}$ include

$$ \bar p_{j-1,r}\vee \bar y_j\vee p_{j,r+1}. $$

If $y_j=0$, the partial sum decreases by one, so for every $r\in{-1,0,1,2}$ include

$$ \bar p_{j-1,r}\vee y_j\vee p_{j,r-1}. $$

The forbidden transitions beyond the allowed range are excluded by

$$ \bar p_{j-1,2}\vee \bar y_j $$

and

$$ \bar p_{j-1,-2}\vee y_j. $$

The first clause prevents the sum from becoming $3$ after adding $1$ to state $2$, and the second prevents the sum from becoming $-3$ after subtracting $1$ from state $-2$.

The one-hot condition for every $j$ consists of the clauses

$$ p_{j,-2}\vee p_{j,-1}\vee p_{j,0}\vee p_{j,1}\vee p_{j,2} $$

and, for every pair of distinct states $r,r'$,

$$ \bar p_{j,r}\vee\bar p_{j,r'}. $$

The resulting formula is satisfiable exactly for strongly balanced sequences. A satisfying assignment gives a unique state $r=A_j$ at every position, and the transition clauses force these states to follow the recurrence defining $A_j$. Conversely, if the sequence is strongly balanced, setting

$$ p_{j,r}=1\iff A_j=r $$

satisfies every clause.

For part (c), fix a positive integer $d\le n$. Apply the construction from part (b) to the subsequence

$$ x_d,x_{2d},\ldots,x_{\lfloor n/d\rfloor d}. $$

The auxiliary variables are indexed as

$$ p^{(d)}_{j,r}, $$

where $j$ is the position inside the $d$th arithmetic progression and $r$ is the corresponding partial signed sum. The resulting clauses force

$$ \left| \sum_{i=1}^{k}(2x_{id}-1) \right|\le2 $$

for every

$$ 1\le k\le \left\lfloor\frac nd\right\rfloor . $$

Taking the conjunction of these clause families over all

$$ 1\le d\le n $$

gives a formula satisfied by

$$ x_1\ldots x_n $$

if and only if every arithmetic subsequence

$$ x_d x_{2d}\ldots x_{\lfloor n/d\rfloor d} $$

is strongly balanced.

The number of arithmetic progressions is $n$. For a fixed $d$, the construction from part (b) uses five state variables for each position in a progression, together with a constant number of clauses per state transition and per one-hot condition. The total size is therefore proportional to

$$ \sum_{d=1}^{n}\left\lfloor\frac nd\right\rfloor, $$

up to the fixed constant factor arising from the finite automaton encoding. This sum is

$$ O(n\log n), $$

because

$$ \sum_{d=1}^{n}\frac nd

n\sum_{d=1}^{n}\frac1d

O(n\log n). $$

Hence the discrepancy condition for all homogeneous arithmetic progressions has a polynomial-size SAT encoding.

Verification

For part (a), the only possible even-index failure would require an even partial sum outside ${-2,0,2}$, but every such value is obtained from an odd predecessor in ${-1,1}$ by adding $\pm1$. The reduction to odd indices is therefore exact.

For part (b), every satisfying assignment to the auxiliary variables determines a path through the five states

$$ -2,-1,0,1,2. $$

The transition clauses allow exactly the changes produced by appending a bit $0$ or $1$. The two boundary clauses remove the only transitions leaving this state set. Thus the encoded language is precisely the strongly balanced sequences.

For part (c), every value of $d$ is treated independently by its own copy of the automaton. A sequence satisfies the final conjunction exactly when each arithmetic subsequence satisfies the clauses from part (b). This proves the required equivalence.

This completes the proof. ∎

Notes

The finite-state encoding is a direct SAT formulation of the bounded discrepancy condition. The state space has only five possible partial sums because the permitted range is fixed, which is why the construction remains polynomial in size.