Polynomial conversion of numeric operators (exactly, at least, at most) to CNF (ala Tseitin)