Trouver le plus petit DFA qui sépare deux mots sans utiliser la recherche par force brute?

Étant donné deux chaînes x et y, je veux créer une taille minimale DFA qui accepte x et rejette y. Une façon de le faire est la recherche par force brute. Vous énumérez les DFA en commençant par le plus petit. Vous essayez chaque DFA jusqu'à ce que vous en trouviez un qui accepte x et rejette y.

Je veux savoir s'il existe un autre moyen connu de trouver ou de créer un DFA de taille minimale qui accepte x et rejette y. En d'autres termes, pouvons-nous battre la recherche par force brute?

Plus de détails:

(1) Je veux vraiment qu'un algorithme trouve une taille minimale DFA, pas une taille DFA proche de la taille minimale.

(2) Je ne veux pas seulement savoir quelle est la taille du DFA minimum.

(3) Ici, je ne me concentre que sur le cas où vous avez deux chaînes x et y.

Modifier :

Informations supplémentaires pour le lecteur intéressé:

Supposons que $x$ et $y$ sont des chaînes binaires de longueur au plus $n$ . C'est un résultat connu qu'il existe un DFA qui accepte $x$ et rejette $y$ avec au plus $\sqrt{n}$ états. Notez qu'il y a environ$n^{\sqrt{n}}$ DFA avec un alphabet binaire et au plus$\sqrt{n}$ états. Par conséquent, l'approche par force brute ne nous obligerait pas à énumérer plus de$n^{\sqrt{n}}$ DFA. Il s'ensuit que l'approche par force brute ne pouvait pas prendre beaucoup plus que$n^{\sqrt{n}}$ temps.

Diapositives que j'ai trouvées utiles: https://cs.uwaterloo.ca/~shallit/Talks/sep2.pdf

Si je devais le faire dans la pratique, j'utiliserais un solveur SAT.

La question de savoir s'il existe un DFA avec états qui accepte x et rejette y peut être facilement exprimée comme une instance SAT. Par exemple, une façon consiste à avoir 2 k 2 variables booléennes: z s , b , t est vrai si le DFA passe de l'état s à l'état t sur le bit d'entrée b . Ajoutez ensuite quelques clauses pour faire en sorte qu'il s'agisse d'un DFA, et quelques variables et clauses pour faire en sorte qu'il accepte x et rejette y .$k$$x$$y$$2k^2$$z_{s,b,t}$$s$$t$$b$$x$$y$

Utilisez maintenant la recherche binaire sur pour trouver le plus petit k tel qu'il existe un DFA de ce type. Sur la base de ce que j'ai lu dans des articles sur un problème connexe, je m'attendrais à ce que cela soit raisonnablement efficace dans la pratique.$k$$k$

D'autres codages de cela comme SAT sont possibles. Par exemple, nous pouvons utiliser un encodage de trace:

• Si est de longueur m , vous pouvez ajouter m lg k variables booléennes: soit s 0 , s 1 , … , s m soit la séquence d'états traversés sur l'entrée x , et représenter chaque s i à l' aide de ⌈ lg k ⌉ variables booléennes.$x$$m$$m\lg k$$s_0,s_1,\dots,s_m$$x$$s_i$$\lceil \lg k \rceil$

• Maintenant, pour chaque tel que x i = x j , vous avez la contrainte que s i - 1 = s j - $i,j$$x_i=x_j$ .$s_{i-1}=s_{j-1} \implies s_i=s_j$

• Ensuite, étendez ceci pour gérer : soit t 0 , … , t n la séquence d'états traversés sur l'entrée y , et représentez chaque t j à l' aide de lg k variables booléennes. Pour chaque i , j tel que y i = y j , ajoutez la contrainte 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 même, pour chaque tel que x i = y j , ajoutez la contrainte que s i - 1 = t j - $i,j$$x_i=y_j$ .$s_{i-1}=t_{j-1} \implies s_i=t_j$

• Les deux traces doivent commencer à partir du même point de départ, donc ajoutez l'exigence que (WLOG vous pouvez exiger s 0 = t 0 = 0 ).$s_0=t_0$$s_0=t_0=0$

• Pour garantir que le DFA n'utilise que états, exigez que 0 ≤ s i < k et 0 ≤ t j < k pour tout i , j .$k$$0 \le s_i < k$$0 \le t_j <k$$i,j$

• Enfin, pour coder l'exigence selon laquelle est accepté et y est rejeté, il faut que s m ≠ t n .$x$$y$$s_m \ne t_n$

Toutes ces exigences peuvent être codées en tant que clauses SAT.

Comme précédemment, vous utiliseriez la recherche binaire sur pour trouver le plus petit k pour lequel un tel DFA existe.$k$$k$