At most $k$ contiguous $\mbox{true}$ values in a Boolean array using SAT

Question

Given an integer $k > 0$ and a Boolean array $A$ of length $n$, find a simplified and efficient CNF formula to ensure that there is not more than $k$ contiguous $\mbox{true}$ values in this array. Examples:

• $k=2$ and $A=[1,1,1,0]$ then it is UNSAT.

• $k=2$ and $A=[1,1,0,1,1,1]$ then it is UNSAT.

• $k=2$ and $A=[1,1,0,1,0,1]$ then it is SAT.

---

Could you help me with some advice, please?

Answer 1

One could use a "sliding window" of length $k+1$ and feed its $k+1$ values into an $\mbox{AND}$ gate with $k+1$ inputs. For example, for $n=6$ and $k=2$, using SymPy:

>>> from sympy import *
>>> x1, x2, x3, x4, x5, x6 = symbols('x1 x2 x3 x4 x5 x6')
>>> f = Not( And(x1,x2,x3) |
             And(x2,x3,x4) |
             And(x3,x4,x5) |
             And(x4,x5,x6) )
>>> to_cnf(f, simplify=True)
(~x1 | ~x2 | ~x3) & (~x2 | ~x3 | ~x4) & (~x3 | ~x4 | ~x5) & (~x4 | ~x5 | ~x6)

Hence, the CNF is

$$ \left(\neg x_{1} \vee \neg x_{2} \vee \neg x_{3}\right) \wedge \left(\neg x_{2} \vee \neg x_{3} \vee \neg x_{4}\right) \wedge \left(\neg x_{3} \vee \neg x_{4} \vee \neg x_{5}\right) \wedge \left(\neg x_{4} \vee \neg x_{5} \vee \neg x_{6}\right) $$

Thus, in each of the $n - k =4$ "windows" there must be at least one $\mbox{False}$ value.

Testing on the examples provided in the question:

>>> f.subs([(x1,1),(x2,1),(x3,0),(x4,1),(x5,1),(x6,1)])
False
>>> f.subs([(x1,1),(x2,1),(x3,0),(x4,1),(x5,0),(x6,1)])
True

Or, using function zip instead,

>>> f.subs(list(zip([x1,x2,x3,x4,x5,x6],[1,1,0,1,0,1])))
True