Consecutive Ones

[APOLOGY: Not too long ago I added to the blog a "feature" provided by Google that hypothetically merges comments made on the blog with comments made to the Google+ post in which I announce the blog entry. I should have read the fine print more carefully. This (a) disenfranchised anyone without a Google account from commenting, (b) hid the presence of comments on the blog until you clicked the "$n$ comments" link, and (c) set $n$ to be the number of comments posted directly to the blog, not the number of comments in the merged stream. The effect of (c) was that this post was showing "0 comments" when in fact there were four or five, all on the G+ post. So I turned off the feature ... which appears to have deleted the existing comments from the G+ post (unless Google is messing with me). Google messing with me is entirely possible: they logged me out in the middle of the edit below, and when I logged back in they had lost all the changes, even though I'd done several previews, which typically has the effect of saving changes. Anyone know if Microsoft recently bought Google??]
 
Stripped of some unnecessary detail, the following showed up on a support forum today: given a set $x_1,\dots,x_n$ of binary variables and a parameter $K$, how can one specify in a mathematical program that (a) $\sum_{i=1}^n x_i$ is either 0 or $K$ and (b) that, in the latter case, the $K$ variables with value 1 must be consecutive?

The first part is easy. Define a new integer variable $s\in\{0,K\}$ and add the constraint $$\sum_{i=1}^n x_i = s.$$Some modeling languages (AMPL comes to mind) allow you to specify directly the domain $\{0,K\}$; in other cases, replace $s$ with $K\hat{s}$ where $\hat{s}$ is a binary variable.

A couple of methods come to mind for enforcing requirement (b). I'll assume that $1<K<n$ to avoid trivial cases. One method is to add the constraints
[BEGIN NONSENSE]
$$\begin{eqnarray*} x_{1} & \le & x_{2}\\ 2x_{j} & \le & x_{j-1}+x_{j+1}\quad \forall j\in\left\{ 2,\dots,n-1\right\} \\ x_{n} & \le & x_{n-1}. \end{eqnarray*}$$[END NONSENSE] 
I suffered a rather severe brain cramp when I wrote the above. Several comments pointed out that this is erroneous. The corrected formulation (which I've tested, and thus post with a modicum of possibly misplaced confidence), is:$$(K-1)(x_{i-1}-x_i)\le \sum_{j=\max(1,i-K)}^{i-2}x_j\quad \forall i\in\{2,\dots,n\}$$(with an empty sum understood to be 0).

Another is to replace binary variable $x_i$ with continuous variable $\tilde{x}_i$ and introduce a new set of binary variables $y_1,\dots,y_{n-K+1}$ where $y_j=1$ signals that $\tilde{x}_j$ starts a run of $K$ consecutive ones. In this approach, we do not need $s$; requirement (a) becomes $$\sum_{i=1}^{n-K+1}y_j \le 1.$$Requirement (b) translates to$$ \tilde{x}_{j}  =  \sum_{i=\max\left\{ 1,j-K+1\right\} }^{j}y_{j}\quad \forall j.$$With the second approach, a presolver can easily eliminate the $\tilde{x}_j$ variables, although it may be preferable to retain them. (Retaining the $\tilde{x}_j$ increases both the number of variables and number of constraints; but in cases where the original $x_j$ appear in more than one expression, eliminating the $\tilde{x}_j$ by substitution increases the density of the constraint matrix.)