DPLL(T)

W informatyce DPLL(T) jest strukturą do określania spełnialności problemów SMT . Algorytm rozszerza oryginalny algorytm DPLL rozwiązujący SAT o możliwość wnioskowania na podstawie dowolnej teorii T . Na wysokim poziomie algorytm działa poprzez przekształcenie problemu SMT w formułę SAT, w której atomy są zastępowane zmiennymi boolowskimi. Algorytm wielokrotnie znajduje satysfakcjonującą wycenę problemu SAT, konsultuje się z osobą rozwiązującą teorię w celu sprawdzenia spójności w ramach teorii specyficznej dla dziedziny, a następnie (jeśli zostanie znaleziona sprzeczność) udoskonala formułę SAT o te informacje.

Wiele nowoczesnych rozwiązań SMT, takich jak Z3 Theorem Prover firmy Microsoft , wykorzystuje DPLL(T) do zasilania swoich podstawowych możliwości rozwiązywania problemów.