ترغب بنشر مسار تعليمي؟ اضغط هنا

Faster One Block Quantifier Elimination for Regular Polynomial Systems of Equations

91   0   0.0 ( 0 )
 نشر من قبل Huu Phuoc Le
 تاريخ النشر 2021
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English




اسأل ChatGPT حول البحث

Quantifier elimination over the reals is a central problem in computational real algebraic geometry, polynomial system solving and symbolic computation. Given a semi-algebraic formula (whose atoms are polynomial constraints) with quantifiers on some variables, it consists in computing a logically equivalent formula involving only unquantified variables. When there is no alternation of quantifiers, one has a one block quantifier elimination problem. This paper studies a variant of the one block quantifier elimination in which we compute an almost equivalent formula of the input. We design a new probabilistic efficient algorithm for solving this variant when the input is a system of polynomial equations satisfying some regularity assumptions. When the input is generic, involves $s$ polynomials of degree bounded by $D$ with $n$ quantified variables and $t$ unquantified ones, we prove that this algorithm outputs semi-algebraic formulas of degree bounded by $mathcal{D}$ using $O {widetilde{~}}left ((n-s+1) 8^{t} mathcal{D}^{3t+2} binom{t+mathcal{D}}{t} right )$ arithmetic operations in the ground field where $mathcal{D} = 2(n+s) D^s(D-1)^{n-s+1} binom{n}{s}$. In practice, it allows us to solve quantifier elimination problems which are out of reach of the state-of-the-art (up to $8$ variables).



قيم البحث

اقرأ أيضاً

Given a straight-line program whose output is a polynomial function of the inputs, we present a new algorithm to compute a concise representation of that unknown function. Our algorithm can handle any case where the unknown function is a multivariate polynomial, with coefficients in an arbitrary finite field, and with a reasonable number of nonzero terms but possibly very large degree. It is competitive with previously known sparse interpolation algorithms that work over an arbitrary finite field, and provides an improvement when there are a large number of variables.
In this paper we report on an application of computer algebra in which mathematical puzzles are generated of a type that had been widely used in mathematics contests by a large number of participants worldwide. The algorithmic aspect of our work pr ovides a method to compute rational solutions of single polynomial equations that are typically large with $10^2 ldots 10^5$ terms and that are heavily underdetermined. This functionality was obtained by adding modules for a new type of splitting of equations to the existing package CRACK that is normally used to solve polynomial algebraic and differential systems.
The only C*-algebras that admit elimination of quantifiers in continuous logic are $mathbb{C}, mathbb{C}^2$, $C($Cantor space$)$ and $M_2(mathbb{C})$. We also prove that the theory of C*-algebras does not have model companion and show that the theory of $M_n(mathcal {O_{n+1}})$ is not $forallexists$-axiomatizable for any $ngeq 2$.
85 - Colin Faverjon 2021
This paper is devoted to the study of the analytic properties of Mahler systems at 0. We give an effective characterisation of Mahler systems that are regular singular at 0, that is, systems which are equivalent to constant ones. Similar characterisa tions already exist for differential and (q-)difference systems but they do not apply in the Mahler case. This work fill in the gap by giving an algorithm which decides whether or not a Mahler system is regular singular at 0.
The satisfiability problem in real closed fields is decidable. In the context of satisfiability modulo theories, the problem restricted to conjunctive sets of literals, that is, sets of polynomial constraints, is of particular importance. One of the central problems is the computation of good explanations of the unsatisfiability of such sets, i.e. obtaining a small subset of the input constraints whose conjunction is already unsatisfiable. We adapt two commonly used real quantifier elimination methods, cylindrical algebraic decomposition and virtual substitution, to provide such conflict sets and demonstrate the performance of our method in practice.
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا