Using Sat solvers for synchronization issues in partial deterministic automata
Formal Languages and Automata Theory
2019-03-27 v1
Abstract
We approach the task of computing a carefully synchronizing word of minimum length for a given partial deterministic automaton, encoding the problem as an instance of SAT and invoking a SAT solver. Our experimental results demonstrate that this approach gives satisfactory results for automata with up to 100 states even if very modest computational resources are used.
Keywords
Cite
@article{arxiv.1903.10549,
title = {Using Sat solvers for synchronization issues in partial deterministic automata},
author = {Hanan Shabana and Mikhail V. Volkov},
journal= {arXiv preprint arXiv:1903.10549},
year = {2019}
}
Comments
15 pages, 3 figures