Я только что узнал о DPLL(T) и алгоритм DPLL по отношению к решателям SMT. Я видел ссылки на z3 в нескольких местах, касающихся решателей SMT.
Интересно, что z3 использует для своих алгоритмов на высоком уровне для реализации решения SMT. Если это алгоритмы DPLL, вариант, что-то нестандартное, куча вещей и т. Д. Надеюсь узнать о различных типах алгоритмов, которые использует современный решатель SMT.
Решатели SMT появились в результате длинного ряда исследований в области автоматизированного мышления, как в компьютерных сообществах по доказательству теорем, так и в традиционной математической логике. Невозможно обобщить все алгоритмы/исследования в ответе на переполнение стека. Тем не менее, книга http://www.decision-procedures.org/ отлично читается, и иметь много ссылок, которые могут помочь вам ориентироваться в литературе. (Первому изданию уже 10 лет, но теперь я вижу, что у них есть второе издание, вышедшее в 2016 году.)
