fast simplifications for tarski formulas
We define the "combinatorial part" of a Tarski formula in which equalities and inequalities are in factored or partially-factored form. The combinatorial part of a formula contains only "monomial inequalities", which are sign conditions on monomials. We give efficient algorithms for answering some basic questions about conjunctions of monomial inequalities and prove the NP-Completeness/Hardness of some others.
simplification tarski formulas