English

Using Sat solvers for synchronization issues in non-deterministic automata

Formal Languages and Automata Theory 2018-01-17 v1

Abstract

We approach the problem of computing a D3D_{3}-synchronizing word of minimum length for a given nondeterministic automaton via its encoding as an instance of SAT and invoking a SAT solver. We also present some experimental results.

Keywords

Cite

@article{arxiv.1801.05391,
  title  = {Using Sat solvers for synchronization issues in non-deterministic automata},
  author = {Hanan Shabana and Mikhail V. Volkov},
  journal= {arXiv preprint arXiv:1801.05391},
  year   = {2018}
}

Comments

16 pages, 4 figures

R2 v1 2026-06-22T23:47:05.375Z