Conflict Driven Clause Learning combined with brute force
Your reasoning is valid, but it won't help a SAT solver go much faster.  Your method produces long clauses that only forbid a single assignment.  What you want to speed up a recursively searching SAT solver is to learn short clauses that forbid many assignments.  That requires a more sophisticated learning strategy than adding a simple disjunction of the negation of the current variable assignment.