Improved SAT models for NFA learning

TL;DR

This paper enhances SAT-based models for learning nondeterministic finite automata from samples by reducing instance size and balancing generation and solving times, with experimental validation of improvements.

Contribution

The paper introduces optimized SAT models for NFA learning that reduce instance complexity and analyze the trade-offs between model size and computational time.

Findings

Significant reduction in SAT instance size.

Trade-off between model generation time and solving efficiency.

Experimental validation of model improvements.

Abstract

Grammatical inference is concerned with the study of algorithms for learning automata and grammars from words. We focus on learning Nondeterministic Finite Automaton of size k from samples of words. To this end, we formulate the problem as a SAT model. The generated SAT instances being enormous, we propose some model improvements, both in terms of the number of variables, the number of clauses, and clauses size. These improvements significantly reduce the instances, but at the cost of longer generation time. We thus try to balance instance size vs. generation and solving time. We also achieved some experimental comparisons and we analyzed our various model improvements.