sympy/sympy — pull request #2964 by SDB1323 (2014-02-25 16:21:10+00:00)
Title: Added Semantic Tableaux. Improved pl_true

1. Added satisfiability checking using a Semantic Tableaux. Semantic tableaux removes the overhead of converting a formula to CNF (or DNF) and is faster than a SAT solver. However, it can only return True or False to indicate satisfiability, and not the model.
2. Modified pl_true to give the correct result under incomplete interpretations. Previously something like pl_true(a >> (b >> a)) would return None. This function now accurately returns whether the value is obvious (True/False) or not (None).