是否可以通過SMT解算器找到布爾公式的最優解？

Question

我有一個很大的布爾公式來解決，由於新版本的原因，我要在這裏粘貼圖片：

而且，我已經一個功能area來衡量的4維整數：area(c,d,e,f)=|c−d|×|e−f|

我想這樣做不僅僅是搞清楚，如果公式是可滿足更多：我在尋找一個最佳的6元組(a,b,c,d,e,f)這使得大公式TRUE和area(c,d,e,f)大於或等於任何尺寸其他6元組也滿足t他的公式。

換句話說，找到Max(area(c,d,e,f)) subjet到大公式。

我想知道SMT解算器是否可以幫助解決這個問題。我知道Z3支持quantifiers，並且能夠說出布爾表達式是否可滿足。但問題是如果Z3可以幫助找到函數area的最佳解決方案。

有沒有人有任何想法？有關SMT解算器，Z3或其他算法的任何意見將讚賞...

Answer 1

總之，是的。

由於您的公式由量詞組成，因此我認爲Microsoft Solver Foundation不是一個合適的選擇。如你所說，Z3支持量詞，整數理論，並用於檢查可滿足性。雖然Z3不直接支持優化，可以使用通用量詞容易編碼優化問題：

坐（A，B，C，d，E，F）=>（forall的A1，B1，C1，D1， e1，f1。sat（a1，b1，c1，d1，e1，f1）& & 目標（a，b，c，d，e，f）> =目標（a1，b1，c1，d1，e1，f1 ））

其中：sat是你的檢查可滿足和goal是area功能，您的優化目標布爾表達式。

正如你所看到的，這個公式是從你的要求中直接翻譯過來的。 (a, b, c, d, e, f)的任務是您需要找到的最佳解決方案。

另一方面，Z3有一個Linux發行版，並提供OCaml API，完全符合您的偏好。

Answer 2

您的問題不完全是可滿足性之一，而是優化或更具體的混合整數編程之一。 這不應該太難以解決使用任何解決方案，如（因爲你標記你的問題Z3，你似乎使用Windows）Microsoft Solver Foundation，它也提供免費版。

Answer 3

目標函數使用非線性整數算術和量詞。 非線性整數算術很難（不可判定） 沒有量詞，加入量詞使其更加糟糕。 如果從INT要真正改變排序，那麼我們有非常 有限的量詞消除非線性雷亞爾 （（設置選項：ELIM_QUANTIFIERS真） （設置選項：ELIM_NLARITH_QUANTIFIERS真）） 但這似乎不真正適合您似乎正在解決的問題。 嘗試查看它是否可以表示爲線性或二次優化問題。 有許多工具可以調整爲二次優化 （並且它們可能較少調整，比如Z3的布爾搜索）。 嘗試一下Solver基金會，它包括幾個優化工具的插件。

可以使用Z3來解決優化問題， 但典型的方法是在Z3的外部 之外有一個循環。首先你提出你想要檢查的問題是可以滿足的，然後你搜索下一個令人滿意的分配，這個分配改善了當前的分配（你從滿意模型中檢索到的） 。 要搜索下一個令人滿意的作業，您將聲明 分配給您要查找的下一個值的'目標'可以改善分配給當前最佳值的'目標' 。

這裏有一些幻燈片http://research.microsoft.com/en-us/people/nbjorner/lecture1.pptx 應該是相關的。他們接近處理這類問題。 該套牌中的最後幾張幻燈片說明了如何使用Z3的API通過 型號進行搜索。如果你想爲輸出格式編寫一個解析器 ，你當然也可以使用文本API。有很多方法可以與Z3進行交互以優化 問題，但它們都需要您在Z3之上編程優化搜索。 如果您的算術和Z3支持的其他域的算術和其他域的布爾組合限制布爾組合，這仍然很有用，但標準優化問題 可以通過專用優化工具更好地解決。

Answer 4

我相信this page將是非常有用的。這個例子已經得到了很好的解釋，它有助於閱讀整篇文章。