将非线性超越算术的可满足性作为证书搜索问题
计算机科学中的逻辑
2025-03-07 v3
摘要
对于典型的一阶逻辑理论，满足赋值具有直接的有限表示，可作为给定赋值满足给定公式的证书。然而，对于增加了三角函数和指数函数的非线性实算术（NTA），尚无已知的满足赋值的直接表示方式，能简单地独立检查所表示的数是否存在并满足给定公式。因此，本文引入了一种不同的NTA可满足性证书形式，并将可满足性问题表述为搜索此类证书的问题。这不仅简化了可满足性的独立验证，也允许设计新算法，通过系统性搜索此类证书来证明可满足性。计算实验表明，所得算法能够证明的可满足性基准问题数量远超现有方法。我们还通过给出相关已知类的下界和上界，刻画了可由此类证书证明可满足性的公式。最后，我们证明了在满足某些鲁棒性假设的公式上，存在终止的NTA公式可满足性检查过程。
引用
@article{arxiv.2303.16582,
title = {Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem},
author = {Enrico Lipparini and Stefan Ratschan},
journal= {arXiv preprint arXiv:2303.16582},
year = {2025}
}