控制Z3的解决策略

Question

所以我们假设我有一个很大的问题需要在Z3中解决，如果我试图在一个解决方案中解决它，它会花费太多的时间。所以我把这个问题分成几部分并分别解决。 作为一个玩具的例子，假设我复杂的问题是要解决那些3个方程：

eq1: x>5 
eq2: y<6 
eq3: x+y = 10 

所以我的问题是，是否例如将有可能首先要解决EQ1和EQ2。然后使用结果解决eq3。

assert eq1 
assert eq2 

(check-sat) 

assert eq3 
(check-sat) 
(get-model) 

似乎工作，但我不知道它是否有意义performancewise？ 增量求解可能会帮助我吗？或者，我还可以使用z3的其他功能来分割我的问题吗？

Answer 1

所考虑的问题通常是可满足性问题，即目标是找到一个一个解决方案（模型）。满足的解决方案（模型）不一定满足eq3，因此您不能将问题减半。我们必须为找到全部解决方案（型号），以便我们可以用该（一组）解决方案替换xeq3。 （例如，这是矩阵对角线后的高斯消元中发生的情况。）