Using Sat solvers for synchronization issues in non-deterministic automata

TL;DR

This paper presents a method to find minimal-length D3-synchronizing words in nondeterministic automata by encoding the problem as a SAT instance and solving it with a SAT solver, supported by experimental results.

Contribution

The paper introduces a novel SAT-based approach to compute minimal D3-synchronizing words for nondeterministic automata, with experimental validation.

Findings

Successful encoding of the synchronization problem as SAT instances.

Effective use of SAT solvers to find minimal D3-synchronizing words.

Experimental results demonstrating the approach's viability.

Abstract

We approach the problem of computing a $D_{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.