Scifaro

中文

ksmt演算是非线性约束的δ-完全决策过程

计算机科学中的逻辑 2021-04-28 v1

作者: Franz Brauße , Konstantin Korovin , Margarita V. Korovina , Norbert Th. Müller

在 arXiv 上查看 ↗ PDF ↗

摘要

ksmt是一种CDCL风格的演算，用于求解涉及多项式和超越函数的实数上的非线性约束。在本文中，我们研究ksmt演算的性质，并证明它是有界问题的δ-完全决策过程。我们还提出了一种带有局部线性化的扩展，其允许对非线性约束进行更高效的处理。

关键词

ksmt演算 δ-完全决策过程非线性约束实数超越函数局部线性化

引用

@article{arxiv.2104.13269,
  title  = {The ksmt calculus is a $\delta$-complete decision procedure for non-linear constraints},
  author = {Franz Brauße and Konstantin Korovin and Margarita V. Korovina and Norbert Th. Müller},
  journal= {arXiv preprint arXiv:2104.13269},
  year   = {2021}
}

备注

The conference version of this paper is accepted at CADE-28