I think it will be useful. One thing that we might want to do in the future is allow SymPy to interface with external SAT solvers written in C, like pycosat. But we wouldn't want to make them hard dependencies of SymPy, so if they are not installed, it would need to fallback to the one written in Python in SymPy.