Программный комплекс предназначен для экспериментального исследования скорости различных вариантов синхронизации недетерминированных конечных автоматов. Он основан на редукции задачи о синхронизации данного недетерминированного автомата словом данной длины к задаче выполнимости для пропозициональных формул с последующим вызовом SAT-солвера, т.е. специализированной программы для решения задачи выполнимости, и состоит из нескольких подпрограмм. Основная подпрограмма кодирует действие букв на состояния автомата с помощью набора формул в конъюнктивной нормальной форме, подобранного так, что этот набор формул выполним тогда и только тогда, когда автомат имеет синхронизирующее слово данной длины. Подпрограмма на входе получает описание автомата в виде некоторого массива и длину потенциального синхронизирующего слова, а на выходе возвращает набор формул в формате DIMACS. Кроме того, программный комплекс включает подпрограммы для генерации случайных автоматов и ряд служебных подпрограмм для накопления и последующей обработки экспериментальных результатов.