Finding the smallest DFA that separates two words without using brute force search?
If I had to do this in practice, I would use a SAT solver.

The question of whether there is a DFA with $k$ states that accepts $x$ and rejects $y$ can be easily expressed as a SAT instance.  For instance, one way is to have $2k^2$ boolean variables: $z_{s,b,t}$ is true if the DFA transitions from state $s$ to state $t$ on input bit $b$.  Then add some clauses to enforce that this is a DFA, and some variables and clauses to enforce that it accepts $x$ and rejects $y$.

Now use binary search on $k$ to find the smallest $k$ such that a DFA of this sort exists.  Based on what I've read in papers on related problem, I would expect that this might be reasonably effective in practice.



Other encodings of this as SAT are possible.  For instance, we can use a trace encoding:


If $x$ is of length $m$, you could add $m\lg k$ boolean variables: let $s_0,s_1,\dots,s_m$ be the sequence of states traversed on input $x$, and represent each $s_i$ using $\lceil \lg k \rceil$ boolean variables.
Now for each $i,j$ such that $x_i=x_j$, you have the constraint that $s_{i-1}=s_{j-1} \implies s_i=s_j$.
Next, extend this to handle $y$: let $t_0,\dots,t_n$ be the sequence of states traversed on input $y$, and represent each $t_j$ using $\lg k$ boolean variables.  For each $i,j$ such that $y_i=y_j$, add the constraint that $t_{i-1}=t_{j-1} \implies t_i=t_j$.
Similarly, for each $i,j$ such that $x_i=y_j$, add the constraint that $s_{i-1}=t_{j-1} \implies s_i=t_j$.
Both traces must start from the same starting point, so add the requirement that $s_0=t_0$ (WLOG you can require $s_0=t_0=0$).
To ensure that the DFA uses only $k$ states, require that $0 \le s_i &lt; k$ and $0 \le t_j &lt;k$ for all $i,j$.
Finally, to encode the requirement that $x$ is accepted and $y$ is rejected, require that $s_m \ne t_n$.


All of these requirements can be encoded as SAT clauses.

As before, you'd use binary search on $k$ to find the smallest $k$ for which such a DFA exists.