Решение уравнений с использованием логики высказываний

Question

Я ищу идеи о том, как кодировать математические уравнения в форму cnf-sat, чтобы их можно было решить с помощью SAT-решения с открытым исходным кодом, такого как MiniSat.

Итак, как мне конвертировать что-то вроде:

3x + 4y - z = 14

-2x - 4z <= -6

x - 3y + z> = 15

в пропозициональное уравнение, которое может быть решено с помощью SAT Solvers.

Любые предложения, потому что я в тупик??

Answer 1

Я предполагаю, что вы ищете целочисленное решение для ваших уравнений, поскольку целочисленное линейное программирование является известной NP-сложной задачей, как и SAT. (Линейное программирование без целочисленного ограничения находится в P, конечно.)

Вы могли бы преобразовать ваши уравнения в экземпляр SAT, но ваше время было бы более плодотворно потрачено на изучение того, как использовать SMT- решатель, что позволит вам гораздо более естественно выразить ваши уравнения. Например, с помощью решателя Microsoft 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 и нажать кнопку воспроизведения, чтобы увидеть, как она решает уравнения.