小编liy*_*stc的帖子

给定任意命题公式PHI（某些变量具有线性约束），确定每个变量的（近似）上限和下限的最佳方法是什么？

一些变量可能是无界的。在这种情况下，算法应得出结论，这些变量没有上限/下限。

例如，PHI =（x = 3 AND y> = 1）。x的上限和下限均为3。y的下限为1，并且y没有上限。

这是一个非常简单的示例，但是是否有一般的解决方案（也许使用SMT求解器）？