TAOCP 7.2.2.2 Exercise 31
The quantity $F_t(r)$ can be found by turning the defining condition into a family of satisfiability problems.
Section 7.2.2.2: Satisfiability
Exercise 31. [28] [28] Let $F_1(r)$ be the smallest $n$ for which there is a bit vector $x_1 \ldots x_n$ with $x_1 + \cdots + x_n = r$ and with no $t$ equally spaced 1s. For example, $F_3(12) = 30$ because of the unique solution 101100011010000000010110001101. Discuss how $F_t(n)$ might be computed efficiently with the help of a SAT solver.
Verified: no
Solve time: 10m20s
Solution
The quantity $F_t(r)$ can be found by turning the defining condition into a family of satisfiability problems. For fixed $t$ and $r$, introduce Boolean variables $x_1,\ldots,x_n$, where $x_i=1$ means that position $i$ is occupied by a $1$ in the bit vector.
The condition
$$ x_1+\cdots+x_n=r $$
is represented by a cardinality constraint requiring exactly $r$ of the variables to be true. This constraint can be encoded as a CNF formula by any standard SAT encoding of cardinality conditions, for example by introducing auxiliary variables for partial sums or sequential counters.
The prohibition of $t$ equally spaced $1$s says that there must not exist integers $a$ and $d>0$ such that
$$ 1\leq a<a+(t-1)d\leq n $$
and
$$ x_a=x_{a+d}=\cdots=x_{a+(t-1)d}=1. $$
For every arithmetic progression
$$ a,a+d,\ldots,a+(t-1)d $$
of length $t$ inside ${1,\ldots,n}$, add the clause
$$ (\bar{x}a\vee \bar{x}{a+d}\vee\cdots\vee \bar{x}_{a+(t-1)d}). $$
This clause excludes exactly the assignments in which all $t$ positions of that progression are equal to $1$. Therefore the resulting CNF formula is satisfiable if and only if there exists a bit vector of length $n$ with exactly $r$ ones and with no $t$ equally spaced ones.
Let this formula be denoted by $S(t,r,n)$. Then
$$ S(t,r,n)\text{ is satisfiable} $$
if and only if
$$ F_t(r)\leq n. $$
Hence $F_t(r)$ can be computed by testing increasing values of $n$ until the first satisfiable instance is found. Since every failed instance proves that no suitable bit vector exists for that value of $n$, the first successful value is exactly the required minimum.
A more efficient computation uses the monotonicity of the condition. If a bit vector of length $n$ exists, then larger values of $n$ can be tested by extending the search space. Thus a SAT solver can be combined with a search procedure such as doubling followed by binary search, whenever a suitable upper bound is available. Each SAT call either produces a witness bit vector or proves that the chosen value of $n$ is too small.
For the example in the statement, the SAT instance for $t=3$, $r=12$, and $n=30$ contains the exact-cardinality constraint
$$ x_1+\cdots+x_{30}=12 $$
together with a clause
$$ (\bar{x}a\vee\bar{x}{a+d}\vee\bar{x}_{a+2d}) $$
for every three-term arithmetic progression in ${1,\ldots,30}$. The solver finds the unique satisfying assignment
$$ 101100011010000000010110001101, $$
showing that
$$ F_3(12)=30. $$
The same construction applies to general $t$ and $r$. The SAT solver does not need to enumerate all $\binom nr$ possible bit vectors, because conflict-driven clause learning can derive consequences from failed partial assignments and reuse them in later parts of the search. The clauses excluding arithmetic progressions are especially suitable for this approach, since each conflict identifies a forbidden pattern of $1$s.
This gives an efficient method for computing $F_t(r)$: construct $S(t,r,n)$, use a SAT solver to decide satisfiability, and search for the smallest $n$ producing a satisfying assignment. The resulting satisfying assignment is a certificate that $F_t(r)\leq n$, while an unsatisfiable SAT result certifies that every smaller value of $n$ fails. ∎