An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination

DOI10.1016/j.tcs.2012.10.020zbMath1291.68433OpenAlexW2998597040MaRDI QIDQ384995

Hitoshi Yanami, Hirokazu Anai, Hidenao Iwane, Kazuhiro Yokoyama

Publication date: 29 November 2013

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2012.10.020

zbMATH Keywords

quantifier elimination cylindrical algebraic decomposition symbolic-numeric computation

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Quantifier elimination, model completeness, and related topics (03C10)

Related Items

CBLIB 2014: a benchmark library for conic mixed-integer and continuous optimization ⋮ Recent Advances in Real Geometric Reasoning ⋮ Mathematics by machine ⋮ Fuzzy simplification of non-numeric expressions containing some intervals and/or floating point numbers ⋮ Sparse interpolation over finite fields via low-order roots of unity ⋮ Multivariate sparse interpolation using randomized Kronecker substitutions ⋮ Computing the differential Galois group of a parameterized second-order linear differential equation ⋮ A new deterministic algorithm for sparse multivariate polynomial interpolation ⋮ A fast algorithm for computing the characteristic polynomial of the p-curvature ⋮ Computing necessary integrability conditions for planar parametrized homogeneous potentials ⋮ Improved algorithm for computing separating linear forms for bivariate systems ⋮ Solving higher order linear differential equations having elliptic function coefficients ⋮ Parallel telescoping and parameterized Picard-Vessiot theory ⋮ A generalized Apagodu-Zeilberger algorithm ⋮ The asymptotic analysis of some interpolated nonlinear recurrence relations ⋮ Fast arithmetic for the algebraic closure of finite fields ⋮ On the computation of the topology of plane curves ⋮ Essentially optimal interactive certificates in linear algebra ⋮ Root counts of semi-mixed systems, and an application to counting nash equilibria ⋮ Synthesis of optimal numerical algorithms using real quantifier elimination (case study: square root computation) ⋮ Sub-cubic change of ordering for Gröbner basis ⋮ Sparse Gröbner bases ⋮ The MMO problem ⋮ Factoring linear differential operators in n variables ⋮ Online order basis algorithm and its impact on the block Wiedemann algorithm ⋮ On isomorphisms of modules over non-commutative PID ⋮ Radical solutions of first order autonomous algebraic ordinary differential equations ⋮ Computing low-degree factors of lacunary polynomials ⋮ Maximum likelihood geometry in the presence of data zeros ⋮ Constructing fewer open cells by GCD computation in CAD projection ⋮ An a posteriori certification algorithm for Newton homotopies ⋮ Evaluating parametric holonomic sequences using rectangular splitting ⋮ Equivariant lattice generators and Markov bases ⋮ Sparse polynomial interpolation codes and their decoding beyond half the minimum distance ⋮ Sparse multivariate function recovery with a high error rate in the evaluations ⋮ Bounds for D-finite closure properties ⋮ Powers of tensors and fast matrix multiplication ⋮ Reduction among bracket polynomials ⋮ Formal solutions of a class of Pfaffian systems in two variables ⋮ On the reduction of singularly-perturbed linear differential systems ⋮ High performance implementation of the TFT ⋮ Randomized detection of extraneous factors ⋮ Toric border basis ⋮ On efficient algorithms for computing parametric local cohomology classes associated with semi-quasihomogeneous singularities and standard bases ⋮ A near-optimal algorithm for computing real roots of sparse polynomials ⋮ LLL reducing with the most significant bits ⋮ Covering of surfaces parametrized without projective base points ⋮ Linear independence oracles and applications to rectangular and low rank linear systems ⋮ Faster relaxed multiplication ⋮ Unimodular completion of polynomial matrices ⋮ Applied Algebraic Geometry in Model Based Design for Manufacturing ⋮ Matrix-F5 algorithms over finite-precision complete discrete valuation fields ⋮ Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1 ⋮ Automatic generation of bounds for polynomial systems with application to the Lorenz system ⋮ Quantifier elimination by cylindrical algebraic decomposition based on regular chains ⋮ Logspace computations in graph products ⋮ Tame decompositions and collisions ⋮ Race Against the Teens – Benchmarking Mechanized Math on Pre-university Problems

Uses Software

Cites Work