We study the satisfiability problem of symbolic tree automata and decompose it into the satisfiability problem of the existential first-order theory of the input characters and the existential monadic second-order theory of the indices of the accepted words. We use our decomposition to obtain tight computational complexity bounds on the decision problem for this automata class and an extension that considers linear arithmetic constraints on the underlying effective Boolean algebra

翻译：我们研究符号树自动机的可满足性问题，并将其分解为输入字符的存在性一阶理论可满足性问题与接受词索引的存在性一元二阶理论可满足性问题。利用该分解，我们获得了此类自动机判定问题的紧计算复杂度界，并进一步扩展至考虑底层有效布尔代数上的线性算术约束的情形。