DPLL algorithm

 This tool solves the satisfiability problem for propositional logic, shortly called SAT. It enables to check whether a formula in propositional logic is satisfiable or not. It also provides a pedagogical demonstration of the DPLL (Davis–Putnam–Logemann–Loveland) algorithm for SAT. If the input formula is not in conjunctive normal form (CNF), then the formula is transformed in an equisatisfiable formula by adding new atomic propositions.