Heuristically matching solution spaces of arithmetic formulas to efficiently reuse solutions