使用命题逻辑求解方程答案

【问题标题】：Solving equations using propositional logic使用命题逻辑求解方程
【发布时间】：2016-03-13 20:58:10
【问题描述】：

我正在寻找有关如何将数学方程编码为 cnf-sat 形式的想法，以便它们可以通过像 MiniSat 这样的开源 SAT 求解器来求解。

那么，我该如何转换：

3x + 4y - z = 14

-2x - 4z

x - 3y + z >= 15

转化为可以使用 SAT Solvers 求解的命题方程。

有什么建议，因为我很难过吗？？

【问题讨论】：

难倒的不仅仅是你。单独的 SAT 求解器无法求解线性程序。而且我坚信任何编码都是一种非常低效的近似。当前的研究提供了将约束求解器与线性规划求解器结合的求解器，但这些系统并未尝试将线性规划编码为 SAT。 x、y 和z 的值域是ℝ?你如何列举ℝ（你没有）？
如果 x、y 和 z 的域被限制为 Z 怎么办？另外，我只是想证明 SAT 可以用来求解算术方程，所以，如果你能帮助我使用约束求解器 (MiniSat) 和其他东西的组合来求解这些方程，那就太好了？
开始搜索该主题的研究论文怎么样？例如Barahona2014，这也给你一些参考和实验。它还明确了一个非常重要的事实：变量的域必须是有限。 ℤ 不是有限的，ℝ 甚至是不可数的。

标签： logic smt bitvector sat sat-solvers

【解决方案1】：

我假设您正在寻找方程的整数解，因为Integer Linear Programming 是一个已知的 NP 难题，SAT 也是如此。（当然，没有整数约束的线性规划在 P 中。）

您可以将方程式转换为 SAT 实例，但您的时间会花在学习如何使用 SMT 求解器上，这将使您更自然地表达方程式。举个例子，使用微软的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 并单击播放按钮以查看它求解方程。

【讨论】：