面向SC-Square的带等式约束CAD的潜力与挑战
符号计算
2017-12-22 v1
摘要
柱形代数分解（CAD）是符号计算中的核心算法，尤其用于实数上的量词消去和更一般的多项式系统求解。它现在正作为可满足性模理论（SMT）求解器在处理非线性实算术时的判定过程而获得日益增多的应用。我们讨论了由SMT应用和SC-Square项目带来的对输入逻辑结构更多关注所带来的潜力，特别是等式约束的存在。我们还强调了利用这些约束所面临的挑战：本原性限制、良定向性问题以及增量性的前景。
引用
@article{arxiv.1711.00312,
title = {The Potential and Challenges of CAD with Equational Constraints for SC-Square},
author = {James H. Davenport and Matthew England},
journal= {arXiv preprint arXiv:1711.00312},
year = {2017}
}
备注
Accepted into proceedings of MACIS 2017