Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition
Matthew England
备注：
Extended Abstract to accompany Invited Talk at CASC 2024
发表信息：
F. Boulier, C. Mou, T.M. Sadykov, and E.V. Vorozhtsov, eds. Computer Algebra in Scientific Computing (Proc. CASC '24), pp. 1-10. (Lecture Notes in Computer Science, vol 14938). Springer International, 2024
This extended abstract accompanies an invited talk at CASC 2024, which surveys recent developments in Real Quantifier Elimination (QE) and Cylindrical Algebraic Decomposition (CAD). After introducing these concepts we will first consider adaptations of CAD inspired by computational logic, in particular the algorithms which underpin modern SAT solvers. CAD theory has found use in collaboration with these via the Satisfiability Modulo Theory (SMT) paradigm; while the ideas behind SAT/SMT have led to new algorithms for Real QE. Second we will consider the optimisation of CAD through the use of Machine Learning (ML). The choice of CAD variable ordering has become a key case study for the use of ML to tune algorithms in computer algebra. We will also consider how explainable AI techniques might give insight for improved computer algebra software without any reliance on ML in the final code.
Chalmers University of Technology and University of Gothenburg（查尔姆斯理工大学和哥德堡大学）；University of Lorraine, CNRS, Inria, LORIA（洛林大学、法国国家科学研究中心、法国研究与发展研究所、洛林计算与自动化实验室）；MPI-INF and Saarland University（德国马克斯·普朗克 informatics 研究所和萨尔兰大学）
KLSS, Institute of Software Chinese Academy of Sciences（中国科学院软件研究所）；University of Chinese Academy of Sciences（中国科学院大学）；University of Oxford（牛津大学）；National Key Laboratory of Space Integrated Information System, Institute of Software Chinese Academy of Sciences（空间信息集成系统国家重点实验室，中国科学院软件研究所）；School of Mathematical Sciences, Peking University（北京大学数学科学学院）；School of Computer Science, Peking University（北京大学计算机学院）；Zhongguancun Laboratory（中关村实验室）
A Design and an Implementation of an Inverse Kinematics Computation in Robotics Using Real Quantifier Elimination based on Comprehensive Gröbner Systems
University of Tsukuba（筑波大学）；Tokiwa Senior High School（常盘高等学校）
An Optimized Path Planning of Manipulator Using Spline Curves and Real Quantifier Elimination Based on Comprehensive Gröbner Systems
Graduate School of Pure and Applied Sciences, University of Tsukuba（筑波大学文理学研究院）；Faculty of Pure and Applied Sciences, University of Tsukuba（筑波大学文理学院）；Faculty of Library, Information and Media Science, University of Tsukuba（筑波大学图书馆、信息与媒体科学学院）
本文提出利用Comprehensive Gröbner System (CGS)与CGS-QE方法高效求解机械臂逆运动学并认证轨迹解，结合三次样条插值与最短路径算法实现路径与关节配置的优化规划。
A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example
Graduate University of Chinese Academy of Sciences（中国科学院大学）；State Key Lab. of Comput. Sci., Institute of Software, CAS（中国科学院软件研究所）；Dept. of Comput. Sci., University of New Mexico（新墨西哥大学）；CISS, CS, Aalborg University（奥尔堡大学）
