Today I've been doing some speed improvements for the logic module. More precisely, I implemented an efficient internal representation for clauses in conjunctive normal form. In practice this means a huge performance boost for all problems that make use the function satisfiable() or dpll_satisfiable(). For example, test_dimacs.py has moved from 2.7 seconds to an impressive 0.3 sec, and ask() runs on average 3x times faster, although both problems still have an overhead because of the conversion to this new representation that can be avoided in most times. Now, the details. Traditionally, dpll (the algorithm that we use for deciding satisfiability) used to store clauses as arrays of symbols, and this worked fine, but sadly comparing symbols in sympy is slow, and this algorithm does a lot of comparisons ... but we can map each sympy symbol to a unique integer, and with minor modifications to the algorithm we get these performance gains. Now, the code. You can pull from my branch logic: git pull http://fa.bianp.net/git/sympy.git logic There are now some obvious performance tweaks we can do: - in ask(), we can skip the conversion to integer representation by 'precompiling' known_facts_dict into this representation. This should be easy and will probably give performance boosts of several orders of magnitude. - this integer representation is very similar to the one used in dimacs CNF files, so a parser that directly converts CNF files to this integer representation should make solving CNF files much faster. --- I would like to give some credit to Ronan Lamy, who sent a patch some time ago, and although I did not include it (yet) into main sympy branch, it inspired me for these modifications.