Я ищу идеи о том, как закодировать математические уравнения в форме cnf-sat, чтобы их можно было решить с помощью SAT-решения с открытым исходным кодом, такого как MiniSat.Решение уравнений с использованием пропозициональной логики
Итак, как преобразовать что-то вроде:
3x + 4y - г = 14
-2x - 4Z < = -6
х - 3y + z> = 15
в пропозициональное уравнение, которое можно решить с помощью SAT Solvers.
Любые предложения, потому что я в тупике ??
Я предполагаю, что вы ищете целочисленное решение для своих уравнений, так как Integer Linear Programming - это известная проблема NP-hard, равно как и SAT. (Конечно, линейное программирование без целочисленного ограничения находится в P.)
Вы можете преобразовать ваши уравнения в экземпляр SAT, но ваше время было бы более плодотворным, если вы научитесь использовать решатель SMT, который позволит вам выразить свою уравнения гораздо более естественно. В качестве примера, используя Z3 solver Microsoft, ваши уравнения выше, могут быть решены с помощью этой простой программы:
(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 и нажмите кнопку воспроизведения, чтобы увидеть его решение уравнений.
Это не только вы в тупике. Решатель 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