Monadic Decomposition - Veanes, Margus; Bjørner, Nikolaj; Nachmanson, Lev; Bereg, Sergey (Journal of the ACM, 2017)
Monadic predicates play a prominent role in many decidable cases, including decision procedures for symbolic automata. We are here interested in discovering whether a formula can be rewritten into a Boolean combination of monadic predicates. Our setting is quantifier-free formulas whose satisfiability is decidable, such as linear arithmetic. Here we develop a semi-decision procedure for extracting a monadic decomposition of a formula when it exists.