# Using Sat solvers for synchronization issues in partial deterministic automata

## TL;DR

This paper presents a SAT-based method for finding minimal carefully synchronizing words in partial deterministic automata, demonstrating effectiveness on automata with up to 100 states using modest resources.

## Contribution

The paper introduces a novel SAT encoding approach for the synchronization problem in partial automata, enabling practical solutions with limited computational resources.

## Key findings

- Effective for automata with up to 100 states
- Satisfactory results with modest computational resources
- New encoding approach improves practical solvability

## 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.