使用命题逻辑求解方程

我正在寻找关于如何将数学方程式编码为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

使用命题逻辑求解方程

回答

相关问题