ДПЛЛ(Т)

В информатике DPLL(T) — это фреймворк для определения выполнимости задач SMT . Алгоритм расширяет исходный алгоритм DPLL , решающий SAT , возможностью рассуждать о произвольной теории T. ^{[1] [2] [3]} На высоком уровне алгоритм работает, преобразуя задачу SMT в формулу SAT, где атомы заменяются булевыми переменными. Алгоритм многократно находит удовлетворяющую оценку для задачи SAT, консультируется с решателем теории для проверки согласованности в рамках теории, специфичной для домена, а затем (если обнаружено противоречие) уточняет формулу SAT с этой информацией. ^[4]

Многие современные решатели SMT, такие как Z3 Theorem Prover и CVC4 от Microsoft , используют DPLL(T) для обеспечения своих основных возможностей решения. ^{[5] [6] [7]}