使用命題邏輯求解方程

我正在尋找關於如何將數學方程式編碼爲cnf-sat形式的想法，以便他們可以通過像MiniSat這樣的開源SAT求解器來解決。使用命題邏輯求解方程

所以，我怎麼轉換是這樣的：

3X + 4Y - Z = 14

-2x - 4Z < = -6

X - 3Y + Z> = 15

成爲可以通過使用SAT求解器求解的命題式。

任何建議，因爲我很難過？

來源

2015-12-08 user3630087

這不僅是你被難倒了。單獨的SAT求解器不能解決線性程序。我堅信任何編碼都是非常低效的近似值。目前的研究提供了求解器，它將*約束求解器與線性程序求解器相結合，但是這些系統不會嘗試將線性程序編碼到SAT中。「x」，「y」和「z」的值域是？你如何列舉ℝ（你沒有）？ – dhke

如果x，y和z的域限制爲Z會怎麼樣？另外，我只是試圖說明SAT可以用來求解算術方程，所以，如果你可以幫助我使用約束求解器（MiniSat）的組合來解決這些方程，那麼會很好嗎？ – user3630087

如何開始搜索有關該主題的研究論文？例如[Barahona2014]（https://www.cs.uic.edu/pub/Isaim2014/WebPreferences/ISAIM2014_Barahona_etal.pdf），這也給你一些參考和實驗。它也清楚表明一個非常重要的事實：變量的域必須是*有限*。 ℤ不是有限的，ℝ甚至不可計數。 – dhke

我假設你正在尋找一個整數解的方程，因爲Integer Linear Programming是一個已知的NP難題，正如SAT一樣。（當然，沒有整數約束的線性編程在P中）

您可以將您的方程式轉換爲SAT實例，但您的時間將花費更多時間學習如何使用解算器，它可以讓您表達您的方程更自然。作爲一個例子，使用微軟的Z3 solver，你的上述公式可以用這個簡單的程序來解決：

(declare-fun x() Int) 
(declare-fun y() Int) 
(declare-fun z() Int) 
(assert (= (+ (* 3 x) (* 4 y) (- z)) 14)) 
(assert (<= (- (* (- 2) x) (* 4 z)) (- 6))) 
(assert (>= (+ (- x (* (- 3) y)) z) 15)) 
(check-sat) 
(get-model)

您可以paste that program爲an online Z3 sandbox和點擊播放按鈕，看看它求解方程。

來源

2015-12-08 21:09:29

使用命題邏輯求解方程

回答

相關問題