Background: DPLL is the algorithm behind SymPy's implementation of logic.inference.satisfiable After reading the original papers by Davis & Putnam [1], I managed to implement a more efficient version of the DPLL algorithm. It is 10x times faster on medium-sized problems (40 variables), and solves some wrong result bugs [2]. As a side effect, the query module has become 2x faster Source code lives in my sympy repo, http:/fa.bianp.net/git/sympy.git, branch logic References: [1]: http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=321034 [2] http://people.sc.fsu.edu/~burkardt/data/cnf/dubois22.cnf