logic - 使用命题逻辑求解方程

Question

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

那么，我该如何转换：

3x + 4y - z = 14

-2x - 4z <= -6

x - 3y + z >= 15

成一个命题方程，可以使用 SAT Solvers 求解。

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

Answer 1

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

您可以将方程式转换为 SAT 实例，但您的时间会花在学习如何使用SMT求解器上，这将使您更自然地表达方程式。举个例子，使用微软的Z3 求解器，你上面的方程可以用这个简单的程序来求解：

(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)

您可以将该程序粘贴到在线 Z3 沙箱中，然后单击播放按钮以查看它求解方程。