Fast simplifications for Tarski formulas based on monomial inequalities (Q420752)

The author proposes and solves several problems of satisfiability and simplification over \(\mathbb{R}\) of conjunctions of monomial inequalities, such as \(x_1x_2^5x_4^2>0\wedge x_2^2x_3\leq0\). This can be extended to more general problems by taking the combinatorial part of the problem; for example, \(ab^2>0\wedge a^2(a+2b)>0\) can be considered as \(x_1x_2^2>0\wedge x_1^2x_3>0\), where \(x_1=a\), \(x_2=b\), \(x_3=a+2b\). Problems under consideration include statements such as \(F\Longrightarrow A\), since \(F\Longrightarrow A\) if and only if \(F\wedge\neg A\) is unsatisfiable. Section 2 considers problems where all the inequalities are strict, and develops an elegant approach to solving the problem by normalizing the inequalities to elements of a vector space \(\mathrm{GF}(2)\) and then using linear algebra. This section includes a discussion that simplification of strict inequalities is in a higher complexity class (NP) than satisfiability (P). Section 3 shows immediately that problems whose inequalities are non-strict require a different approach, as the set of normalized inequalities is not isomorphic to a vector space. Development of such an approach is not pursued further. Section 4 considers the mixed case, normalizing each statement to vectors over \(\mathrm{GF}(2)\) again, using a form where the strict and non-strict inequalities are separated. This allows one to consider the satisfiability of the strict inequalities alone, as the non-strict inequalities are easily satisfiable (\(x_i=0\)). Section 5 describes a polynomial-time algorithm that simplifies the non-strict part of monomial inequalities. This algorithm also reveals equations implied by the input formula. The author points out that ``simplification'' of a formula is a term for which one can choose different metrics, and considers two: the sum of the total degrees of the monomials, and the sum of the number of variables appearing in each monomial. The author argues that the latter metric is more relevant, as it is agrees with the first metric in the case of strict inequalities, and is a better measure of the simplicity of expressions such as \(x\leq0\) and \(x^2\leq0\). A number of examples illustrate the problems and results, and leads the reader carefully through the reasoning. Section 7 consists entirely of computational examples. An earlier publication in ISSAC 2009 contains much of the same material; this version contains additional results, such as an algorithm to solve the simplification problem for conjunctions of non-strict monomials in polynomial time.