一般情况
这不仅仅是效率问题。考虑一个有两个变量的问题a and b，和一个单一的约束：
a != b
范围是多少b？ （最大还是其他？）
你可以说所有的价值观都是合法的。但这是错误的，因为显然选择a影响选择b。周围的变量越多，问题就会变得越复杂。我认为在这种情况下问题还没有得到很好的定义，因此寻找解决方案（有效或其他）没有多大意义。
单变量假设
话虽如此，我认为你can如果您假设系统中只有一个变量，请想出一个解决方案。 （或者，如果您将所有其他变量固定为一些预定义的常量。）如果您愿意走这条路，那么您可以实现二分搜索算法，通过简单地证明量化公式来找到合理大小的范围
Exists([b], And(b >= minBound, b <= maxBound, Not(constraints)))
一旦你得到unsat为此，你有你的范围。只要你得到sat，你可以调整你的minBound/maxBound在较小的范围内进行搜索。在最坏的情况下，这可能会变成线性行走，但您可以通过确保在每个步骤中显着减小大小来“减少”此搜索。这可能是整个搜索的一个参数，具体取决于您希望间隔有多大。必须在尝试找到最大范围和您想在搜索中花费多长时间之间进行选择。当然，如果削减太多，可能会错过一个很大的区间，但这就是效率的代价。
Example1（好的情况）有一个约束说b != 5。然后你的搜索会很快，并且根据你要去哪个分支，你会找到[0, 4] or [6, 255]假设8位字。
Example2（坏情况）有一个约束说b is even。然后你的搜索将表现出最坏情况的行为，如果你的“削减”大小是 1，你可能会迭代 255 次才能确定[0, 0];假设z3为您提供每次调用中的最大奇数。
我希望这能说明这一点。不过，总的来说，我认为您会更接近实际应用的“好案例”，即使您的缩减尺寸很小，您也很可能在几次迭代中收敛。当然，这完全取决于您的问题领域，但我希望它通常适用于软件分析。
