  Grammatical inference consists in learning a formal grammar (as a set of
rewrite rules or a finite state machine). We are concerned with learning
Nondeterministic Finite Automata (NFA) of a given size from samples of positive
and negative words. NFA can naturally be modeled in SAT. The standard model [1]
being enormous, we also try a model based on prefixes [2] which generates
smaller instances. We also propose a new model based on suffixes and a hybrid
model based on prefixes and suffixes. We then focus on optimizing the size of
generated SAT instances issued from the hybrid models. We present two
techniques to optimize this combination, one based on Iterated Local Search
(ILS), the second one based on Genetic Algorithm (GA). Optimizing the
combination significantly reduces the SAT instances and their solving time, but
at the cost of longer generation time. We, therefore, study the balance between
generation time and solving time thanks to some experimental comparisons, and
we analyze our various model improvements.
