×

zbMATH — the first resource for mathematics

Exact DFA identification using SAT solvers. (English) Zbl 1291.68192
Sempere, JosĂ© M. (ed.) et al., Grammatical inference: Theoretical results and applications. 10th international colloquium, ICGI 2010, Valencia, Spain, September 13–16, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-15487-4/pbk). Lecture Notes in Computer Science 6339. Lecture Notes in Artificial Intelligence, 66-79 (2010).
Summary: We present an exact algorithm for identification of deterministic finite automata (DFA) which is based on satisfiability (SAT) solvers. Despite the size of the low level SAT representation, our approach is competitive with alternative techniques. Our contributions are fourfold: First, we propose a compact translation of DFA identification into SAT. Second, we reduce the SAT search space by adding lower bound information using a fast max-clique approximation algorithm. Third, we include many redundant clauses to provide the SAT solver with some additional knowledge about the problem. Fourth, we show how to use the flexibility of our translation in order to apply it to very hard problems. Experiments on a well-known suite of random DFA identification problems show that SAT solvers can efficiently tackle all instances. Moreover, our algorithm outperforms state-of-the-art techniques on several hard problems.
For the entire collection see [Zbl 1195.68011].

MSC:
68Q32 Computational learning theory
68Q45 Formal languages and automata
Software:
PicoSAT
PDF BibTeX XML Cite
Full Text: DOI