Davis–Putnam–Logemann–Loveland Algorithm (Satisfiability Modulo Theory)

Definition