可以SMT/Z3被如所描述的用於優化調度

Question

能SMT求解器有效地找到爲僞布爾問題的解決方案（或賦值）如下：

\sum {i..m} f_i x1 x2.. xn *w_i 

其中f_i x1 x2 .. xn是一個布爾函數，並w_i是Int類型的權重。

爲了方便起見，我重點介紹了第1頁和第3頁的內容，這些內容足以說明僞布爾問題 。

Answer 1

SMT求解器通常解決這個問題：給定一個邏輯公式，可選地使用來自基礎理論（例如算術理論，位向量理論，數組）的函數和謂詞，是可滿足與否的公式。 它們通常不會爲您指定目標函數 並且通常沒有內置的優化過程。

一些特殊情況是僅使用布爾值或布爾值組合以及位矢量或整數的公式。僞布爾約束可以用整數或編碼（考慮到溢出語義考慮一些注意事項）使用位向量來表示，或者它們可以直接編碼到SAT中。對於使用有限整數的一些公式，這些整數屬於假布爾型問題，Z3將嘗試自動縮減爲位向量。這僅適用於標記爲QF_LIA的SMT-LIB2格式的Benchmkars，或者在您明確調用執行此減少的策略（應用「qflia」策略）時適用。

雖然Z3不直接暴露目標函數，但在研究界積極追求具有目標函數的SMT求解器的問題 。 Nieuwenhuis和Oliveras在SAT 2006中提出的一種方法是將 作爲一種習慣理論解決「加權最大SMT」問題。 Yices內置 加權最大SMT功能，Z3沒有，但可以編寫自定義的 理論執行加權最大SMT解算器的回溯搜索，但沒有任何 開箱即用。

有時人們試圖用量化的公式來指定目標函數。 理論上，人們可能希望量詞消除程序可以爲目標解決 。 當涉及到性能時，這通常很糟糕。量詞消除 是一種過度使用，並且例程（我們有）將不會有效。