TAOCP 7.2.2.2 Exercise 117

Let $\nu x = x_1 + \cdots + x_n$ and $\nu^{(2)}x = x_1x_2 + x_2x_3 + \cdots + x_{n-1}x_n$.

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

Exercise 117. [23] [23] Given a sequence $x = x_1 \ldots x_n$, let $\nu^{(2)}x = x_1 x_2 + x_2 x_3 + \cdots + x_{n-1} x_n$. (A similar sum appears in the serial correlation coefficient, 3.3.2–(23).)

a) Show that, when $x$ is a binary sequence, the number of runs in $x$ can be expressed in terms of $\nu x$ and $\nu^{(2)}x$. b) Explain how to encode the condition $\nu^{(2)}x \le r$ as a set of clauses, by modifying the cardinality constraints (20)–(21) of Bailleux and Boufkhad. c) Similarly, encode the condition $\nu^{(2)}x \ge r$.

Verified: yes
Solve time: 1m05s

Solution

Let $\nu x = x_1 + \cdots + x_n$ and $\nu^{(2)}x = x_1x_2 + x_2x_3 + \cdots + x_{n-1}x_n$.

(a)

A run begins at position $1$ and at every index $i \in {2,\ldots,n}$ where $x_{i-1} \ne x_i$. Hence the number of runs is

$1 + \sum_{i=1}^{n-1} (x_i \oplus x_{i+1}).$

For binary variables,

$x_i \oplus x_{i+1} = x_i + x_{i+1} - 2x_ix_{i+1}.$

Therefore the number of runs equals

$1 + \sum_{i=1}^{n-1}(x_i + x_{i+1} - 2x_ix_{i+1}).$

The linear part satisfies

$\sum_{i=1}^{n-1} x_i + \sum_{i=1}^{n-1} x_{i+1} = (x_1 + \cdots + x_{n-1}) + (x_2 + \cdots + x_n) = 2\nu x - x_1 - x_n.$

The quadratic part is $2\nu^{(2)}x$. Substitution gives

$\text{runs}(x) = 1 + 2\nu x - x_1 - x_n - 2\nu^{(2)}x.$

Thus

$\boxed{\text{runs}(x) = 1 + 2\nu x - x_1 - x_n - 2\nu^{(2)}x}.$

(b)

Introduce a new variable $z_i$ for each adjacent pair, intended to represent

$z_i \equiv x_i \land x_{i+1}, \qquad 1 \le i \le n-1.$

This equivalence is enforced by clauses

$(\bar{z}_i \lor x_i), \qquad (\bar{z}i \lor x{i+1}), \qquad (z_i \lor \bar{x}i \lor \bar{x}{i+1}).$

Then

$\nu^{(2)}x = \sum_{i=1}^{n-1} z_i.$

The condition $\nu^{(2)}x \le r$ becomes a cardinality constraint on the variables $z_1,\ldots,z_{n-1}$. Using the Bailleux–Boufkhad sequential counter encoding from (20)–(21), introduce auxiliary counter variables $s_{i,j}$ representing

$s_{i,j} = \sum_{k=1}^i z_k \ge j.$

The standard clauses enforcing monotonicity and recurrence of the counter are applied unchanged to the sequence $(z_i)$, and the bound is enforced by forbidding $s_{n-1,r+1} = 1$.

Thus the original quadratic constraint is reduced to a linear cardinality constraint over the variables $z_i$ together with local consistency clauses defining each $z_i$.

(c)

The condition $\nu^{(2)}x \ge r$ is expressed as

$\sum_{i=1}^{n-1} z_i \ge r.$

Using the same sequential counter variables $s_{i,j}$, this is enforced by requiring

$s_{n-1,r} = 1.$

Equivalently, in clause form, one forbids all assignments in which fewer than $r$ of the $z_i$ are true, implemented by the same counter construction as in (b) but with the final constraint asserting attainment of level $r$.

This completes the solution. ∎