我正在處理Z3中的有理數線性問題。要使用Z3，我會使用SBV。
我提出的問題的一個例子是：
import Data.SBV
solution1 = do
x <- sRational "x"
w <- sRational "w"
constrain $ x.< w
constrain $ x 2*w .>=0 .|| x .== 1
我的問題是：
這類問題可以判定嗎？我找不到可判定理論的串列或判斷理論是否可判定的方法。我找到的最接近的是this。關于實數的理論是可判定的，但對于有理數來說是否一樣？直覺告訴我確實如此，但我還沒有找到讓我確信的資訊。
提前致謝
uj5u.com熱心網友回復：
SBV 使用標準的“兩個整數”思想對有理數建模；也就是說，它將分子和分母分別表示為整數。這意味著如果您添加兩個符號有理數，您將在整數上有一個非線性項。因此，理論上，問題將出現在半可判定片段中。也就是說，即使您將乘法限制為具體的標量，符號有理數的加法也會導致整數上的非線性項。
話雖如此，我在使用理性時還是很幸運的。其中 z3 能夠毫不費力地決定大多數感興趣的問題。如果它被證明是一個問題，你應該切換到SReal型別（即代數實數），z3 有一個決策程序。但是，當然，您得到的模型現在可以包括代數實數，例如 2 的平方根等（即任何具有整數系數的多項式的根。）
旁注如果您的問題允許 delta-sat（即擾動的可滿足性），您應該查看 dReal ( http://dreal.github.io )，SBV 也支持它作為后端求解器。但也許這不是你的想法。
理論說明
嚴格來說，有理數上的線性算術是可判定的；有關證明，請參見https://www.cs.ox.ac.uk/people/james.worrell/lecture15-2015.pdf的第 3 節。但是，SMT 求解器不開箱即用地支持理性；和 SBV（正如我上面提到的），使用兩個符號整數來表示有理數。因此，添加兩個有理數會導致兩個符號整數相乘，從而使您脫離可判定片段。當然，在實踐中，即使存在非線性項，求解器也非常善于提出解決方案。只是你并不總是得到保證。因此，對您的問題的更嚴格的回答是，雖然對有理數的線性算術是可判定的，但 SBV 使用的轉換將問題置于非線性整數算術域中，因此無法保證可判定性。在任何情況下，SMTLib 都沒有理性理論，因此在對它們的一流支持方面，您有點不走運。
uj5u.com熱心網友回復：
我猜如果對適當縮放的約束集合存在整數解決方案，則將存在合理的解決方案。例如，x=1/2(=5/10), w=3/5(=6/10)是您的示例問題的解決方案。將您的問題縮放 10，我們有等效的約束集：
10*x < 10*w
(10*x 20*w >= 0) || (10*x == 10)
寫x'=10*x和w'=10*w，這意味著這x'=5, w'=6是一個整數解：
x' < w'
(x' w' >= 0) || (x' == 10)
Presburger 著名地表明一階邏輯加整數和加法是可判定的。（也允許乘以常數，因為它可以擴展為加法——例如 3*x 是 x x x。）
我想剩下的唯一技巧是表明可以在尚未解決問題的情況下選擇要使用的縮放比例。我沒有想到任何明顯的事情，但是這應該是可行的似乎是合理的。例如，如果你取約束集中所有非零分子和分母的乘積，你可以證明以該乘積作為分母的有理數集與完整的有理數集沒有區別。（如果是這樣，您可以查看證明，看看它是否仍然適用于較小的分母。）
我不是 z3 專家，所以我不能談論這如何轉化為該工具是否特別合適，但在我看來，創建一個合適的工具是可能的。
轉載請註明出處，本文鏈接：https://www.uj5u.com/qukuanlian/444373.html