Davis–Putnam–Logemann–Loveland Algorithm