SAT can be solved surprisingly quickly via superposed bools on Interaction Nets (gist.github.com)

The description of interaction nets sounds a bit like hash-consing, with some extra optimisations.