这是 problem 的 z3 统计数据在 Non-Linear Integer Real Fragment 中(我的很多问题都与此类似):
(:add-rows 11062574
:added-eqs 34
:arith-conflicts 37293
:assert-lower 837747
:assert-upper 1909779
:binary-propagations 13807730
:bound-prop 32666
:conflicts 47631
:decisions 157457
:del-clause 32828
:final-checks 39307
:gcd-tests 329820
:gomory-cuts 927
:ineq-splits 19490
:memory 39.52
:minimized-lits 93912
:mk-clause 73468
:pivots 768193
:propagations 15992318
:pseudo-nonlinear 254856
:restarts 41
:time 151.65
:total-time 151.68)
由于问题是非线性的，我相信单纯形技术并没有直接用于解决这个问题(尽管我在输出中看到了一些类似单纯形的统计数据)。基于 earlier回应，我理解存在整数的非线性实数技术是基于 Grobner 基的，相关函数在 theory_arith* 中。是否有论文/一些文档可以找到关于在 z3 中为此片段实现的技术的具体信息？
此外，虽然问题本身是非线性的，但非线性的唯一出现涉及两个变量的乘法(并且有一些这样的表达式)，并且其中一个变量只能取幂的值两个并由一些简单的约束约束/定义:
(const1 <= |a| < const2) => (var-a = const1)
其中 const1 和 const2 是两个连续的正幂。因此，var-a 表示小于或等于 |a| 的两个最大幂。这些变量被声明为 Real 类型。
特别好奇，因为我在统计输出中看到一个术语 pseudo-nonlinear。约束是否以某种方式在内部线性化？另外，是否有更好的方法来编码这些约束，以便 z3 在此类问题上做得更好？
最佳答案
请参阅以下相关问题:
以下也可能是相关的:
关于z3 - 哪些技术用于处理 z3 中的非线性整数实数问题？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/21247410/