Are there any techniques for checking whether a clause is subsumed by another clause when adding it to a cnf formula?
There is a preprocessing method called vivification$^1$ that can be used to detect subsumed clauses.  It relies on unit propagation to work.

To vivify a clause, make a partial variable assignment such that all the proposed clause's literals are false.  E.g. if your proposed clause is $x_1 \lor \lnot{x_2} \lor x_3 \lor \lnot{x_4}$, assign $x_1$ = FALSE, $x_2$ = TRUE, $x_3$ = FALSE, and $x_4$ = TRUE.  If while you're doing these assignments unit propagation produces a conflict, or if one of the variables is set by unit propagation and vivification later wants to set it to a different value, then the new clause is implied by the existing formula and can be discarded as redundant.



$^1$"Vivifying Propositional Clausal Formulae" by Cédric PIETTE,
Youssef HAMADI and Lakhdar SAÏS