Fast simplifications for Tarski formulas based on monomial inequalities

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.NEWLINENEWLINESection 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\)).NEWLINENEWLINESection 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\).NEWLINENEWLINEA number of examples illustrate the problems and results, and leads the reader carefully through the reasoning. Section 7 consists entirely of computational examples.NEWLINENEWLINEAn 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.

Recommendations

Cites work

Cited in

(7)

Describes a project that uses

Uses Software

SYNRAC

This page was built for publication: Fast simplifications for Tarski formulas based on monomial inequalities

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q420752)