The ksmt calculus is a d-complete decision procedure for non-linear constraints
The ksmt calculus is a d-complete decision procedure for non-linear constraints
复制标题
ksmt 演算是非线性约束的 d 完全决策过程
DOI：
10.1016/j.tcs.2023.114125
复制
发表时间：
2023
影响因子：
1.1
通讯作者：
Brauße F
中科院分区：
文献类型：
--
作者：
Brauße F
ksm 是一种 CDCL 风格的微积分，用于解决涉及多项式和超越函数的实数的非线性约束。在本文中，我们研究了 ksmt 微积分的性质，并证明它是有界问题的 δ 完全决策过程。为此，我们提供基于非线性函数的均匀或局部连续性模计算线性化的具体算法。后一种方法称为局部线性化，并且被证明具有足以终止的所需属性，并且还允许更有效地处理非线性约束。我们构建线性化的方法基于可计算分析，特别是我们引入了实数的柯西兼容紧致表示，并证明其名称是局部紧致的，允许更有效地计算局部线性化，同时保持δ完整性。
ksmtis a CDCL-style calculus for solving non-linear constraints over the real numbers involving polynomials and transcendental functions. In this article we investigate properties of theksmtcalculus and show that it is aδ-complete decision procedure for bounded problems. For that purpose we provide concrete algorithms computing linearisations based on either uniform or local moduli of continuity of non-linear functions. The latter method is called local linearisation and is shown to have desirable properties sufficient for termination and which also allow for more efficient treatment of non-linear constraints. Our methods for constructing linearisations are based on computable analysis, in particular we introduce the Cauchy-compatible compact representation of reals and prove its names to be locally compact, allowing for more efficient computation of local linearisations while maintainingδ-completeness.