QuantifierElimination
CylindricalAlgebraicDecompose
produce the full CAD for a set of polynomials, or the set of polynomials associated to a Tarski formula
Calling Sequence
Parameters
Returns
Description
Examples
Compatibility
CylindricalAlgebraicDecompose( A, E, opts )
A
-
a list or set of polynomials, or a list or set of relations on polynomials, or a full real Tarski formula, or a single polynomial or relation to produce the CAD for. All such polynomials passed in A are interpreted as inequations, unless they appear as equations in a Tarski formula, whereby they are interpreted as equational constraints
E
(optional) a polynomial, an equation, or a list or set of such to be used as equational constraints for the produced CAD
opts
core keyword options for cylindrical algebraic decomposition (see QuantifierElimination options)
A CADData object that contains data structures for the CAD.
Builds a full Cylindrical Algebraic Decomposition (CAD), (Lazard and) sign invariant for the polynomials according to input. Unlike PartialCylindricalAlgebraicDecompose, this procedure will not attempt any evaluation of truth values and hence no quantifier elimination (QE), although it can accept a (quantified) Tarski formula as input. If quantifiers are included in a formula, they will be ignored.
The method of constructing the CAD is a Lazard projection followed by standard lifting. No strategy for lifting is included, considering the whole CAD must be constructed in all circumstances. If equational constraints are provided via E, then these will be used in a reduced projection operator for the first projection.
If equational constraints can be found in a Tarski formula A, then these will be used in a reduced projection operator if possible.
Information on keyword options for the routine can be found in the help page QuantifierElimination options.
with⁡QuantifierElimination
CylindricalAlgebraicDecompose,DeleteFormula,InsertFormula,PartialCylindricalAlgebraicDecompose,QuantifierEliminate,QuantifierTools
A≔x−3,x2+y2−2
C≔CylindricalAlgebraicDecompose⁡A
C≔Variables=⁢y,xInput Polynomials=⁢x−3y2+7y2−2x2+y2−2# Cells=⁢23Projection polynomials for level 1=⁢y2+7y2−2Projection polynomials for level 2=⁢x−3x2+y2−2
Examine the leaf cells for the CAD of polynomials in A:
GetCells⁡C
Description=⁢RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856<y∧3<xSample Point=⁢y=3,x=4Index=⁢5,3,Description=⁢RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856<y∧x=3Sample Point=⁢y=3,x=3Index=⁢5,2,Description=⁢RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856<y∧x<3Sample Point=⁢y=3,x=2Index=⁢5,1,Description=⁢y=RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856∧3<xSample Point=⁢y=RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856,x=4Index=⁢4,5,Description=⁢y=RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856∧x=3Sample Point=⁢y=RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856,x=3Index=⁢4,4,Description=⁢y=RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856∧0<x∧x<3Sample Point=⁢y=RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856,x=1Index=⁢4,3,Description=⁢y=RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856∧x=0Sample Point=⁢y=RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856,x=0Index=⁢4,2,Description=⁢y=RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856∧x<0Sample Point=⁢y=RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856,x=−1Index=⁢4,1,Description=⁢RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624<y∧y<RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856∧3<xSample Point=⁢y=0,x=4Index=⁢3,7,Description=⁢RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624<y∧y<RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856∧x=3Sample Point=⁢y=0,x=3Index=⁢3,6,Description=⁢RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624<y∧y<RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856∧RootOf⁡_Z2+y2−2,index=real2<x∧x<3Sample Point=⁢y=0,x=2Index=⁢3,5,Description=⁢RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624<y∧y<RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856∧x=RootOf⁡_Z2+y2−2,index=real2Sample Point=⁢y=0,x=RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856Index=⁢3,4,Description=⁢RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624<y∧y<RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856∧RootOf⁡_Z2+y2−2,index=real1<x∧x<RootOf⁡_Z2+y2−2,index=real2Sample Point=⁢y=0,x=0Index=⁢3,3,Description=⁢RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624<y∧y<RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856∧x=RootOf⁡_Z2+y2−2,index=real1Sample Point=⁢y=0,x=RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624Index=⁢3,2,Description=⁢RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624<y∧y<RootOf⁡_Z2−2,208701085205324515393147573952589676412928..417402170410649030813295147905179352825856∧x<RootOf⁡_Z2+y2−2,index=real1Sample Point=⁢y=0,x=−3Index=⁢3,1,Description=⁢y=RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624∧3<xSample Point=⁢y=RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624,x=4Index=⁢2,5,Description=⁢y=RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624∧x=3Sample Point=⁢y=RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624,x=3Index=⁢2,4,Description=⁢y=RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624∧0<x∧x<3Sample Point=⁢y=RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624,x=1Index=⁢2,3,Description=⁢y=RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624∧x=0Sample Point=⁢y=RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624,x=0Index=⁢2,2,Description=⁢y=RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624∧x<0Sample Point=⁢y=RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624,x=−1Index=⁢2,1,Description=⁢y<RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624∧3<xSample Point=⁢y=−3,x=4Index=⁢1,3,Description=⁢y<RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624∧x=3Sample Point=⁢y=−3,x=3Index=⁢1,2,Description=⁢y<RootOf⁡_Z2−2,−796131459065725562949953421312..−15922629181314231125899906842624∧x<3Sample Point=⁢y=−3,x=2Index=⁢1,1
Examine the number leaf cells for the CAD of the formula F:
F≔And⁡x2+y2−z2+2<0,y<z,x<y
F≔x2+y2−z2<−2∧y<z∧x<y
C≔CylindricalAlgebraicDecompose⁡F
C≔Variables=⁢z,x,yInput Polynomials=⁢xzx−yx−zy−zx2+2z2+2z2−22⁢x2−z2+2x2−z2+2x2+y2−z2+2# Cells=⁢287Projection polynomials for level 1=⁢zz2+2z2−2Projection polynomials for level 2=⁢xx−zx2+22⁢x2−z2+2x2−z2+2Projection polynomials for level 3=⁢x−yy−zx2+y2−z2+2
NumberOfLeafCells⁡C
287
Get the sample point for a cell of C:
GetSamplePoint⁡GetCells⁡C1
z=3,x=4,y=5
The QuantifierElimination:-CylindricalAlgebraicDecompose command was introduced in Maple 2023.
For more information on Maple 2023 changes, see Updates in Maple 2023.
See Also
PartialCylindricalAlgebraicDecompose
QuantifierElimination options
Download Help Document