It would be good to have the chance to do basic graph queries on the clausal graph of the cnf theory. Either networkx or python-graph would work.