Using a satisfiability solver to identify deterministic finite state automata

M.J.H. Heule, S.E. Verwer

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)
    1 Downloads (Pure)


    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 seems to be competitive with alternative techniques. Our contributions are threefold: 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. Experiments on a well-known suite of random DFA identification problems show that SAT solvers can efficiently tackle all instances. Moreover, our exact algorithm outperforms state-of-the-art techniques on several hard problems.
    Original languageEnglish
    Title of host publicationProceedings of the 21st Benelux Conference on Artificial Intelligence (BNAIC 2009, Eindhoven, The Netherlands, October 29-30, 2009)
    EditorsT. Calders, K. Tuyls, M. Pechenizkiy
    Publication statusPublished - 2009


    Dive into the research topics of 'Using a satisfiability solver to identify deterministic finite state automata'. Together they form a unique fingerprint.

    Cite this