The talk focuses on (i) providing some insight of state-of-the-art
Davis-Longeman-Loveland (DLL) solvers and (ii) on comparing Stalmarck's
calculus and DLL algorithm/calculus from an high-level perspective.
The purpose is to guide the audience to a better understanding of "modern"
SAT solvers, in order to see how they can be used to tackle formal