確定任意命題公式中變量的上下限

Question

給定任意命題公式PHI（對某些變量的線性約束），確定每個變量的（近似）上下限的最佳方法是什麼？

某些變量可能是無界的。在這種情況下，算法應該得出結論：這些變量沒有上/下限。例如，PHI =（x = 3 AND y> = 1）。 x的上下界都是3. y的下界是1，y沒有上界。

這是一個非常簡單的例子，但總體上有沒有解決方案（可能使用SMT解算器）？

Answer 1

這假設每個變量的SAT/UNSAT域是連續的。

1. 使用SMT解算器檢查公式的解決方案。如果沒有解決方案，那就意味着沒有上/下限，所以停下來。
2. 對於公式中的每個變量，在變量的域中執行兩個二進制搜索，一個搜索下限，另一個搜索上限。搜索每個變量的起始值是步驟1中找到的解決方案中變量的值。使用SMT求解器探測每個搜索值的可滿足性，並有條不紊地將每個變量的邊界括起來。

僞用於搜索功能碼，假設整數域變量：

lower_bound(variable, start, formula) 
{ 
    lo = -inf; 
    hi = start; 
    last_sat = start; 
    incr = 1; 
    do { 
     variable = (lo + hi)/2; 
     if (SMT(formula) == UNSAT) { 
      lo = variable + incr; 
     } else { 
      last_sat = variable; 
      hi = variable - incr; 
     } 
    } while (lo <= hi); 
    return last_sat; 
} 

和

upper_bound(variable, start, formula) 
{ 
    lo = start; 
    hi = +inf; 
    last_sat = start; 
    do { 
     variable = (lo + hi)/2; 
     if (SMT(formula) == SAT) { 
      last_sat = variable; 
      lo = variable + incr; 
     } else { 
      hi = variable - incr; 
     } 
    } while (lo <= hi); 
    return last_sat; 
} 

-inf/+ INF是最小/最大值在每一個域所能表述變量。如果lower_bound返回-inf，那麼該變量沒有下界。如果upper_bound返回+ inf，那麼變量沒有上限。

Answer 2

實際上，大多數此類優化問題需要在SMT解算器之上進行某種形式的迭代 - 直到 - 最大/最小類型的外部驅動程序。量化方法也可以利用SMT解算器的特定功能，但實際上這種約束對於底層解算器來說太難了。特別參見這個討論：How to optimize a piece of code in Z3? (PI_NON_NESTED_ARITH_WEIGHT related)

話雖如此，大多數高級語言綁定包括簡化您的生活所必需的機制。舉例來說，如果你使用哈斯克爾SBV庫腳本Z3，你可以有：

Prelude> import Data.SBV 
Prelude Data.SBV> maximize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1] 
Prelude Data.SBV> maximize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) 
Nothing 
Prelude Data.SBV> minimize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1] 
Prelude Data.SBV> minimize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1] 

第一個結果狀態x = 3，Y = 1最大程度地增強相對於X謂詞X == 3 & &ÿ > = 1。 第二個結果表明，沒有任何值可以最大化y關於同一個謂詞。 第三次調用表示x = 3，y = 1使關於x的謂詞最小化。 第四次調用表示x = 3，y = 1使關於y的謂詞最小化。 （有關詳細信息，請參見http://hackage.haskell.org/packages/archive/sbv/0.9.24/doc/html/Data-SBV.html#g:34）。

您也可以使用選項「迭代」（而不是量化）來讓庫迭代地執行優化，而不是使用量詞。這兩種技術是而不是相當於後者可能陷入局部最小/最大值，但迭代方法可能解決量化版本對於SMT求解器來說處理太多的問題。