¿Encuentra el DFA más pequeño que separa dos palabras sin usar la búsqueda de fuerza bruta?

Dadas dos cadenas x e y, quiero construir un DFA de tamaño mínimo que acepte x y rechace y. Una forma de hacerlo es la búsqueda de fuerza bruta. Enumera los DFA que comienzan con los más pequeños. Intenta cada DFA hasta que encuentre uno que acepte x y rechace y.

Quiero saber si hay alguna otra forma conocida de encontrar o construir un DFA de tamaño mínimo que acepte x y rechace y. En otras palabras, ¿podemos superar la búsqueda de fuerza bruta?

Mas detalle:

(1) Realmente quiero un algoritmo para encontrar un DFA de tamaño mínimo, no un DFA de tamaño mínimo.

(2) No solo quiero saber qué tan grande o pequeño es el DFA mínimo.

(3) Aquí, solo estoy enfocado en el caso en el que tienes dos cadenas x e y.

Editar :

Información adicional para el lector interesado:

Supongamos que e son cadenas binarias de longitud como máximo . Es un resultado conocido que hay un DFA que acepta y rechaza con como máximo estados. Observe que hay aproximadamente DFA con un alfabeto binario y como máximo estados. Por lo tanto, el enfoque de la fuerza bruta no requeriría que enumeremos más de DFA. De ello se deduce que el enfoque de la fuerza bruta no podría tomar mucho más que tiempo.$x$$y$$n$$x$$y$$\sqrt{n}$$n^{\sqrt{n}}$$\sqrt{n}$$n^{\sqrt{n}}$$n^{\sqrt{n}}$

Diapositivas que encontré útiles: https://cs.uwaterloo.ca/~shallit/Talks/sep2.pdf

Si tuviera que hacer esto en la práctica, usaría un solucionador SAT.

La cuestión de si hay un DFA con estados que acepta x y rechaza y se puede expresar fácilmente como una instancia SAT. Por ejemplo, una forma es tener 2 k 2 variables booleanas: z s , b , t es verdadero si el DFA pasa del estado s al estado t en el bit de entrada b . Luego agregue algunas cláusulas para hacer cumplir que esto es un DFA, y algunas variables y cláusulas para hacer cumplir que acepta x y rechaza y .$k$$x$$y$$2k^2$$z_{s,b,t}$$s$$t$$b$$x$$y$

Ahora use la búsqueda binaria en para encontrar la k más pequeña de manera que exista un DFA de este tipo. Según lo que he leído en documentos sobre problemas relacionados, esperaría que esto sea razonablemente efectivo en la práctica.$k$$k$

Otras codificaciones de esto como SAT son posibles. Por ejemplo, podemos usar una codificación de rastreo:

• Si es de longitud m , puede agregar m lg k variables booleanas: sea s 0 , s 1 , ... , s m la secuencia de estados recorridos en la entrada x , y represente cada s i usando ⌈ lg k ⌉ variables booleanas.$x$$m$$m\lg k$$s_0,s_1,\dots,s_m$$x$$s_i$$\lceil \lg k \rceil$

• Ahora para cada tal que x i = x j , tiene la restricción de que s i - 1 = s j - $i,j$$x_i=x_j$ .$s_{i-1}=s_{j-1} \implies s_i=s_j$

• Luego, extienda esto para manejar : deje que t 0 , ... , t n sea ​​la secuencia de estados recorridos en la entrada y , y represente cada t j usando variables booleanas lg k . Para cada i , j tal que y i = y j , agregue la restricción de que t i - 1 = t j - $y$$t_0,\dots,t_n$$y$$t_j$$\lg k$$i,j$$y_i=y_j$ .$t_{i-1}=t_{j-1} \implies t_i=t_j$

• De manera similar, para cada tal que x i = y j , agregue la restricción que s i - 1 = t j - $i,j$$x_i=y_j$ .$s_{i-1}=t_{j-1} \implies s_i=t_j$

• Ambas trazas deben comenzar desde el mismo punto de partida, por lo tanto, agregue el requisito de que (WLOG puede requerir s 0 = t 0 = 0 ).$s_0=t_0$$s_0=t_0=0$

• Para asegurarse de que el DFA usa solo estados, requiere que 0 ≤ s i < k y 0 ≤ t j < k para todo i , j .$k$$0 \le s_i < k$$0 \le t_j <k$$i,j$

• Finalmente, para codificar el requisito de que es aceptado y y es rechazado, requiere que s m ≠ t n .$x$$y$$s_m \ne t_n$

Todos estos requisitos pueden codificarse como cláusulas SAT.

Como antes, usaría la búsqueda binaria en para encontrar la k más pequeña para la que existe tal DFA.$k$$k$