Satisfiability Modulo the Theory of Nonlinear Real Arithmetic, SMT(NRA) for short, concerns the satisfiability of polynomial formulas, which are quantifier-free Boolean combinations of polynomial equations and inequalities with integer coefficients and real variables. In this paper, we propose a local search algorithm for a special subclass of SMT(NRA), where all constraints are strict inequalities. An important fact is that, given a polynomial formula with $n$ variables, the zero level set of the polynomials in the formula decomposes the $n$-dimensional real space into finitely many components (cells) and every polynomial has constant sign in each cell. The key point of our algorithm is a new operation based on real root isolation, called cell-jump, which updates the current assignment along a given direction such that the assignment can `jump' from one cell to another. One cell-jump may adjust the values of several variables while traditional local search operations, such as flip for SAT and critical move for SMT(LIA), only change that of one variable. We also design a two-level operation selection to balance the success rate and efficiency. Furthermore, our algorithm can be easily generalized to a wider subclass of SMT(NRA) where polynomial equations linear with respect to some variable are allowed. Experiments show the algorithm is competitive with state-of-the-art SMT solvers, and performs particularly well on those formulas with high-degree polynomials.


翻译:满足非线性实数算术理论,即SMT(NRA),涉及多项式公式的满足性问题,这些公式是具有整数系数和实数变量的量词自由布尔组合的多项式方程和不等式。在本文中,我们针对一个特殊的SMT(NRA)子类提出了一种局部搜索算法,其中所有约束条件都是严格不等式。一个重要事实是,对于给定的$n$个变量的多项式公式,公式中多项式的零级集将实数空间分解成有限的组件(单元格),并且每个多项式在每个单元格中都有恒定的符号。我们算法的关键是一种基于实根分离的新操作,称为单元格跳跃,它在沿着给定方向更新当前赋值的情况下对赋值进行“跳跃”,以便赋值可以从一个单元格跳跃到另一个单元格。一个单元环节可以调整多个变量的值,而传统的局部搜索操作(如SAT中的翻转和SMT(LIA)中的关键移动)仅改变一个变量的值。我们还设计了一个两级操作选择,以平衡成功率和效率。此外,我们的算法可以轻松推广到更广泛的SMT(NRA)子类,其中允许多项式方程相对于某些变量是线性的。实验表明,该算法在与最新的SMT求解器竞争时表现优异,并且在具有高次多项式的公式中表现特别好。

0
下载
关闭预览

相关内容

【硬核书】稀疏多项式优化:理论与实践,220页pdf
专知会员服务
66+阅读 · 2022年9月30日
【硬核书】矩阵代数基础,248页pdf
专知会员服务
83+阅读 · 2021年12月9日
【CIKM2020】神经逻辑推理,Neural Logic Reasoning
专知会员服务
49+阅读 · 2020年8月25日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
生成扩散模型漫谈:最优扩散方差估计(上)
PaperWeekly
0+阅读 · 2022年9月25日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2023年5月11日
Arxiv
0+阅读 · 2023年5月9日
Arxiv
0+阅读 · 2023年5月8日
VIP会员
相关资讯
生成扩散模型漫谈:最优扩散方差估计(上)
PaperWeekly
0+阅读 · 2022年9月25日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员