Fast simplifications for Tarski formulas based on monomial inequalities

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. By simplifying the combinatorial part of a Tarski formula, and mapping the simplified combinatorial part back to a Tarski formula, we obtain non-trivial simplifications without algebraic operations.