@article{veanes2017monadic,
author = {Veanes, Margus and Bjørner, Nikolaj and Nachmanson, Lev and Bereg, Sergey},
title = {Monadic Decomposition},
year = {2017},
month = {May},
abstract = {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.},
publisher = {ACM},
url = {http://approjects.co.za/?big=en-us/research/publication/monadic-decomposition-2/},
journal = {Journal of the ACM},
volume = {64},
chapter = {2},
edition = {Journal of the ACM},
}