Finding the smallest DFA that separates two words without using brute force search?

Question

Given two strings x and y, I want to build a minimum size DFA that accepts x and rejects y. One way to do this is brute force search. You enumerate DFA's starting with the smallest. You try each DFA until you find one that accepts x and rejects y.

I want to know if there is any other known way of finding or building a minimum size DFA that accepts x and rejects y. In other words, can we beat brute force search?

More Detail:

(1) I really do want an algorithm to find a minimum size DFA, not a near minimum size DFA.

(2) I don't just want to know how large or small the minimum DFA is.

(3) Right here, I'm only focused on the case were you have two strings x and y.

---

Edit:

Additional information for the interested reader:

Suppose $x$ and $y$ are binary strings of length at most $n$. It is a known result that there is a DFA that accepts $x$ and rejects $y$ with at most $\sqrt{n}$ states. Notice that there are about $n^{\sqrt{n}}$ DFA's with a binary alphabet and at most $\sqrt{n}$ states. Therefore, the brute force approach wouldn't require us to enumerate through more than $n^{\sqrt{n}}$ DFA's. It follows that the brute force approach couldn't take much more than $n^{\sqrt{n}}$ time.

Slides that I found helpful: https://cs.uwaterloo.ca/~shallit/Talks/sep2.pdf

Answer 1

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 < k$ and $0 \le t_j <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.