Given an equation, represented by words on left side and the result on right side.
You need to check if the equation is solvable under the following rules:
Each character is decoded as one digit (0 - 9).
Every pair of different characters they must map to different digits.
Each words[i] and result are decoded as one number without leading zeros.
Sum of numbers on left side (words) will equal to the number on right side (result). 
Return True if the equation is solvable otherwise return False.
Example 1:
Input: words = ["SEND","MORE"], result = "MONEY"
Output: true
Explanation: Map 'S'-> 9, 'E'->5, 'N'->6, 'D'->7, 'M'->1, 'O'->0, 'R'->8, 'Y'->'2'
Such that: "SEND" + "MORE" = "MONEY" ,  9567 + 1085 = 10652
Example 2:
Input: words = ["SIX","SEVEN","SEVEN"], result = "TWENTY"
Output: true
Explanation: Map 'S'-> 6, 'I'->5, 'X'->0, 'E'->8, 'V'->7, 'N'->2, 'T'->1, 'W'->'3', 'Y'->4
Such that: "SIX" + "SEVEN" + "SEVEN" = "TWENTY" ,  650 + 68782 + 68782 = 138214
Example 3:
Input: words = ["THIS","IS","TOO"], result = "FUNNY"
Output: true
Example 4:
Input: words = ["LEET","CODE"], result = "POINT"
Output: false
Constraints:
2 <= words.length <= 5
1 <= words[i].length, result.length <= 7
words[i], result contains only upper case English letters.
Number of different characters used on the expression is at most 10.
class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        max_len = len(result)
        if max(len(w) for w in words) > max_len:
            return False
        words = [word.rjust(max_len, '#') for word in words]
        result = result.rjust(max_len, '#')
        equations = list(zip(result, *words))
        used_digits = set()
        nonzero_chars = set(equations[0])
        assignments = {'#':0}
        def isSAT(eqn_index, carry):
            if eqn_index<0:
                return carry == 0
            remaining_terms = []
            for t in equations[eqn_index]:
                if t not in assignments:
                    for guess in range(10):
                        if guess in used_digits:
                            continue
                        if guess == 0 and t in nonzero_chars:
                            continue
                        assignments[t] = guess
                        used_digits.add(guess)
                        if isSAT(eqn_index, carry):
                            return True
                        del assignments[t]
                        used_digits.remove(guess)
                    return False
            
            s = sum(assignments[c] for c in equations[eqn_index][1:]) + carry
            if s % 10 != assignments[equations[eqn_index][0]]:
                return False
            else:
                return isSAT(eqn_index - 1, s // 10)
           
        return isSAT(max_len-1, 0)
class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        max_len = len(result)
        if max(len(w) for w in words) > max_len:
            return False
        words = [word.rjust(max_len, '#') for word in words]
        result = result.rjust(max_len, '#')
        equations = list(zip(result, *words))
        used_digits = set()
        nonzero_chars = set(equations[0])
        assignments = {'#':0}
        def isSAT(eqn_index, carry):
            if eqn_index<0:
                return carry == 0
            remaining_terms = []
            for t in equations[eqn_index]:
                if t not in assignments:
                    for guess in range(10):
                        if guess in used_digits:
                            continue
                        if guess == 0 and t in nonzero_chars:
                            continue
                        assignments[t] = guess
                        used_digits.add(guess)
                        if isSAT(eqn_index, carry):
                            return True
                        del assignments[t]
                        used_digits.remove(guess)
                    return False
            
            s = sum(assignments[c] for c in equations[eqn_index][1:]) + carry
            if s % 10 != assignments[equations[eqn_index][0]]:
                return False
            else:
                return isSAT(eqn_index - 1, s // 10)
           
        return isSAT(max_len-1, 0)