suppose that two SAT formulas on different variables $F_1, F_2$ are given on the input that are known to be true and the problem is to build an algorithm that finds a solution to each. the formulas actually are generated by another algorithm which creates/ generates instances $F_n$ for any $n$. the solving algorithm can find/ exploit "similar structures" contained in each by analyzing eg the clause-variable graph, eg looking for graph isomorphisms etc.
has this problem of finding "similarities" between two SAT formulas by a solver been studied?
there is some rough connection of this eg implications of worst case bounds in this paper A simple proof that AND-compression of NP-complete problems is hard (Dell), but am looking for more direct algorithm(s) and possibly more empirical approaches/ analysis, eg somewhat similar to strategies/ heuristics used in SAT solver implementations. (this problem has applications in eg automated theorem proving.)