Making Cylindrical Algebraic Decomposition more problem-sensitive
副标题:
时间:2018-04-04 来源:数学机械化重点实验室
题目: Making Cylindrical Algebraic Decomposition more problem-sensitive
报告人: James Davenport (University of Bath)
时间地点: 2018.04.20 15:00pm N202
摘要: Collins' [?] original motivation for Cylindrical Algebraic Decomposition was to solve Quanti_er Elimination over the reals, i.e. reduce 8xk+19xk+2 _ _ _ _(x1; : : : ; xn) to (x1; : : : ; xk ), where _and are boolean combinations of polynomial equalities and inequalities. A CAD for this is also a CAD for any other problem involving the same polynomials with the quanti_ed variables in the same order (but possibly di_erent quanti_ers). This seems like overkill. [?] showed how to do better if _ can be viewed as f = 0 ^ _.
This therefore handles _ := (f1 = 0 ^ g1 > 0) _ (f2 = 0 ^ g2 > 0) by writing it as f1f2 = 0 ^ _. We showed in [?] how to handle _directly, and more e_ciently. In [?] we extended this to cases like _ := (f1 = 0 ^ g1 > 0) _ g2 > 0, where there is no equational constraint.
We will desribe these methods, and how they can extend to multiple equational constraints.