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: 1m03s

---

Solution

Let

$$ \nu x=x_1+x_2+\cdots+x_n $$

as in the notation of Section 7.2.2.2, and let

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

(a)

For a binary sequence, a change of value between two consecutive positions contributes one new run. Hence the number of runs is one plus the number of indices $i$ with $1\le i<n$ for which $x_i\ne x_{i+1}$.

For binary variables,

$$ x_i\ne x_{i+1} $$

is represented by

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

Therefore the number of changes is

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

The first two sums telescope as

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

so

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

After simplifying,

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

2\nu x-x_1-x_n-2\nu^{(2)}x . $$

Adding the initial run gives

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

This formula also holds for the constant sequences: if all $x_i=0$, it gives one run, and if all $x_i=1$, it gives one run.

(b)

Introduce auxiliary variables

$$ z_i=x_ix_{i+1}\qquad(1\le i<n). $$

The condition

$$ \nu^{(2)}x\le r $$

is equivalent to

$$ z_1+z_2+\cdots+z_{n-1}\le r . $$

Each $z_i$ is defined by the three clauses

$$ \bar{x}i\vee \bar{x}{i+1}\vee z_i , $$

$$ x_i\vee \bar{z}_i , $$

and

$$ x_{i+1}\vee \bar{z}_i . $$

The first clause forces $z_i=1$ whenever both $x_i$ and $x_{i+1}$ are $1$, while the other two clauses force $z_i=0$ whenever either input is $0$. Hence these clauses give exactly

$$ z_i=x_ix_{i+1}. $$

Now apply the Bailleux-Boufkhad cardinality construction from (20)-(21) to the $n-1$ variables

$$ z_1,\ldots,z_{n-1} $$

instead of the original variables. The resulting clauses encode precisely

$$ \sum_{i=1}^{n-1}z_i\le r, $$

and together with the defining clauses for the $z_i$ they encode

$$ \nu^{(2)}x\le r . $$

(c)

The condition

$$ \nu^{(2)}x\ge r $$

can be converted into an upper-bound condition by complementing the auxiliary variables. Since

$$ \nu^{(2)}x=z_1+\cdots+z_{n-1}, $$

we have

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

Equivalently,

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

Therefore the same Bailleux-Boufkhad cardinality clauses encode the condition by using the literals

$$ \bar z_1,\ldots,\bar z_{n-1} $$

as the inputs and setting the bound to

$$ n-1-r . $$

The variables $z_i$ are still defined by the conjunction clauses above, so the resulting formula is satisfiable exactly for those binary sequences satisfying

$$ \nu^{(2)}x\ge r . $$

This completes the solution. ∎