After some hacking on the queries module, I finally got it right without the limitations of past versions. You can check it out from my repo http://fa.bianp.net/git/sympy.git, branch master. It now relies even more on logic.inference.satisfiable(), which is just an implementation of the DPLL algorithm. Bad news is that (my implementation of ) dpll_satisfiable() is SLOW, so inevitably queries are SLOW. But everything is not lost, since the algorithm is quite fast, and in fact other variants of the algorithm (MiniSAT) perform 6600x times faster than my implementation on medium-sized problems (60 variables, 170 clauses). So this looks like something smells bad on the programming side ... However, I spent the day profiling the function (link to source code used for profiling) without much success