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.

Difficulty: interview

Starter code:

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        

Solutions:
class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        longest_word = max([len(word) for word in words])
        if len(result) != longest_word and len(result) != longest_word + 1:
            return False
        
        result_indices = []
        acc = 0
        all_chars = []
        front_indices = []
        for i in range(1, longest_word + 1):
            for word in words:
                if i == len(word):
                    front_indices.append(acc)
                if i <= len(word):
                    all_chars.append(word[i * -1])
                    acc += 1
            if i == len(result):
                front_indices.append(acc)
            result_indices.append(acc)
            acc += 1
            all_chars.append(result[i * -1])

        if len(result) > longest_word:
            result_indices.append(acc)
            front_indices.append(acc)
            all_chars.append(result[0])
            
        self.words = words
        self.result = result
        self.result_indices = result_indices
        self.all_chars = all_chars
        self.mappings = {}
        self.used_chars = set()
        self.front_indices = front_indices
        
        return self.backtrack(0, 0)
        
    def backtrack(self, current_i: int, carry: int) -> bool:
        if current_i == len(self.all_chars):
            if self.mappings[self.result[0]] == 0:
                return False
            return True
        
        cur_char = self.all_chars[current_i]

        if current_i in self.result_indices:
            code, new_carry = self.verify(self.result_indices.index(current_i), carry)
            if code == 0:
                return False
            else:
                if self.backtrack(current_i + 1, new_carry):
                    return True
                
                if code == 2:
                    self.used_chars.remove(self.mappings[cur_char])
                    del self.mappings[cur_char]
                    
                return False
                    
        if cur_char in self.mappings:
            if current_i in self.front_indices and self.mappings[cur_char] == 0:
                return False
            return self.backtrack(current_i + 1, carry)
        
        for i in range(10):
            if current_i in self.front_indices and i == 0:
                continue
            if i not in self.used_chars:
                self.mappings[cur_char] = i
                self.used_chars.add(i)
                
                if self.backtrack(current_i + 1, carry):
                    return True

                del self.mappings[cur_char]
                self.used_chars.remove(i)
                
        return False
            
    def verify(self, index: int, carry: int) -> (int, int):
        cur_sum = carry
            
        for word in self.words:
            if index < len(word):
                cur_sum += self.mappings[word[index * -1 -1]]

        carry = int(cur_sum / 10)
        cur_sum = cur_sum % 10
            
        result_char = self.result[index * -1 - 1]
        if result_char in self.mappings:
            if self.mappings[result_char] != cur_sum:
                return 0, 0
            else:
                return 1, carry
        else:
            if cur_sum in self.used_chars:
                return 0, 0
            self.mappings[result_char] = cur_sum
            self.used_chars.add(cur_sum)
            return 2, carry
        

                


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
        level = [[word[-i-1] for word in words if i<len(word)] for i in range(max_len)]
        level_set = [set([result[-i-1]] + level[i]) for i in range(max_len)]
        used_digits = set()
        nonzero_chars = set(word[0] for word in words + [result])
        assignments = {}
        def isSAT(eqn_index, carry):
            if eqn_index >= max_len:
                return carry == 0
            remaining_terms = []
            for t in level_set[eqn_index]:
                if t not in assignments:
                    for guess in range(t in nonzero_chars, 10):
                        if guess in used_digits:
                            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 level[eqn_index]) + carry
            if s % 10 != assignments[result[-eqn_index-1]]:
                return False
            return isSAT(eqn_index +1, s // 10)
           
        return isSAT(0, 0)

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        words.append(result)
        M, N = len(words), max(list(map(len, words)))
        dic = {}
        rem = [None] * 10
        lead = set([w[0] for w in words])

        def backtrack(i, j, cur):
            if j == N:
                return cur == 0
            if i == M:
                return not cur % 10 and backtrack(0, j + 1, cur // 10)
            if j >= len(words[i]):
                return backtrack(i + 1, j, cur)
            t = words[i][~j]
            sign = 1 if i < M - 1 else -1
            if t in dic:
                return backtrack(i + 1, j, cur + dic[t] * sign)
            else:
                for k, r in enumerate(rem):
                    if not r and (k or t not in lead):
                        dic[t] = k
                        rem[k] = t
                        if backtrack(i + 1, j, cur + dic[t] * sign):
                            return True
                        del dic[t]
                        rem[k] = None
            return False

        return backtrack(0, 0, 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
        level = [[word[-i-1] for word in words if i<len(word)] for i in range(max_len)]
        level_set = [set([result[-i-1]] + level[i]) for i in range(max_len)]
        used_digits = set()
        nonzero_chars = set(word[0] for word in words + [result])
        assignments = {}
        def isSAT(eqn_index, carry):
            if eqn_index >= max_len:
                return carry == 0
            for t in level_set[eqn_index]:
                if t not in assignments:
                    for guess in range(t in nonzero_chars, 10):
                        if guess in used_digits:
                            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 level[eqn_index]) + carry
            if s % 10 != assignments[result[-eqn_index-1]]:
                return False
            return isSAT(eqn_index +1, s // 10)
           
        return isSAT(0, 0)

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        if max([len(w) for w in words]) > len(result):
            return False
        lead_letters = set([w[0] for w in words + [result]])

        letters = []
        for k in range(1, len(result) + 1):
            for w in words:
                if len(w) >= k and w[-k] not in [x[0] for x in letters]:
                    letters.append((w[-k], k))
            letters.append((result[-k], -k))

        # print(letters)

        letter2num = {}
        num2letter = ['']*10
        nums = '0123456789'

        def helper(k):
            if k == len(letters):
                return True
            letter, digit = letters[k][0], letters[k][1]
            if digit < 0:
                left = sum([int(''.join([letter2num[ch] for ch in w[digit:]])) for w in words])
                if left < 10 ** (-digit-1):
                    return False
                num = int(str(left)[digit])
                if letter not in letter2num and not num2letter[num]:
                    letter2num[letter] = str(num)
                    num2letter[num] = letter
                    if helper(k + 1):
                        return True
                    letter2num.pop(letter)
                    num2letter[int(num)] = ''
                elif num2letter[num] != letter or (letter in letter2num and letter2num[letter] != str(num)):
                    return False
                else:
                    return helper(k + 1)

            else:
                if letter not in letter2num:
                    num_range = nums if letter not in lead_letters else nums[1:]
                    for num in num_range:
                        if not num2letter[int(num)]:
                            letter2num[letter] = num
                            num2letter[int(num)] = letter
                            if helper(k+1):
                                return True
                            letter2num.pop(letter)
                            num2letter[int(num)] = ''
                    return False
                else:
                    return helper(k + 1)

        return helper(0)

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        n = len(result)
        if max(len(w) for w in words) > n:
            return False
        
        level = [[w[-k - 1] for w in words if k < len(w)] for k in range(n)]
        level_set = [set(level[k]) | {result[-k - 1]} for k in range(n)]
        leading = set(w[0] for w in words) | {result[0]}
        val = {k: None for k in set.union(set(result), *(set(w) for w in words))}
        used = set()
        
        def search(k, carry):
            if k == n:
                return carry == 0
            
            for c in level_set[k]:
                if val[c] is None:
                    for v in range(c in leading, 10):
                        if v not in used:
                            val[c] = v
                            used.add(v)
                            if search(k, carry):
                                return True
                            val[c] = None
                            used.remove(v)
                    return False
                
            s = sum(val[c] for c in level[k]) + carry
            if s % 10 != val[result[-k - 1]]:
                return False
            return search(k + 1, s // 10)

        return search(0, 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
        use_count = Counter(''.join(words +[result]))
        level = [[word[-i-1] for word in words if i<len(word)] for i in range(max_len)]
        level_set = [set([result[-i-1]] + level[i]) for i in range(max_len)]
        used_digits = set()
        nonzero_chars = set(word[0] for word in words + [result])
        assignments = {}
        def isSAT(eqn_index, carry):
            if eqn_index >= max_len:
                return carry == 0
            remaining_terms = [t for t in level_set[eqn_index] if t not in assignments]
            if remaining_terms:
                term_to_guess = max(remaining_terms, key=lambda x:use_count[x])
                for guess in range(term_to_guess in nonzero_chars, 10):
                    if guess in used_digits:
                        continue
                    assignments[term_to_guess] = guess
                    used_digits.add(guess)
                    if isSAT(eqn_index, carry):
                        return True
                    del assignments[term_to_guess]
                    used_digits.remove(guess)
                return False
            
            s = sum(assignments[c] for c in level[eqn_index]) + carry
            if s % 10 != assignments[result[-eqn_index-1]]:
                return False
            return isSAT(eqn_index +1, s // 10)
           
        return isSAT(0, 0)

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        self.words = words
        self.result = result
        self.front_chars = set([word[0] for word in words] + [result[0]])    
        self.result_indices = []
        self.all_chars = []
        
        new_words = words + [result]
        while len(new_words) > 0:
            for i in range(len(new_words)):
                self.all_chars.append(new_words[i][-1])
                new_words[i] = new_words[i][:-1]
            self.result_indices.append(len(self.all_chars) - 1)
            new_words = [word for word in new_words if len(word) > 0]

        self.mappings = {}
        self.used_chars = set()
        
        return self.backtrack(0, 0)
        
    def backtrack(self, current_i: int, carry: int) -> bool:
        if current_i == len(self.all_chars):
            return True
        
        cur_char = self.all_chars[current_i]

        if current_i in self.result_indices:
            code, new_carry = self.verify(self.result_indices.index(current_i), carry)
            if code == 0:
                return False
            else:
                if self.backtrack(current_i + 1, new_carry):
                    return True
                
                if code == 2:
                    self.used_chars.remove(self.mappings[cur_char])
                    del self.mappings[cur_char]
                    
                return False
                    
        if cur_char in self.mappings:
            return self.backtrack(current_i + 1, carry)
        
        for i in range(10):
            if cur_char in self.front_chars and i == 0:
                continue
            if i not in self.used_chars:
                self.mappings[cur_char] = i
                self.used_chars.add(i)
                
                if self.backtrack(current_i + 1, carry):
                    return True

                del self.mappings[cur_char]
                self.used_chars.remove(i)
                
        return False
            
    def verify(self, index: int, carry: int) -> (int, int):
        cur_sum = carry
            
        for word in self.words:
            if index < len(word):
                cur_sum += self.mappings[word[index * -1 -1]]

        carry = int(cur_sum / 10)
        cur_sum = cur_sum % 10
            
        result_char = self.result[index * -1 - 1]
        if result_char in self.mappings:
            if self.mappings[result_char] != cur_sum:
                return 0, 0
            else:
                return 1, carry
        else:
            if cur_sum in self.used_chars:
                return 0, 0
            if result_char in self.front_chars and cur_sum == 0:
                return 0, 0
            
            self.mappings[result_char] = cur_sum
            self.used_chars.add(cur_sum)
            return 2, carry
        

                


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        def backtrack(ch_pos_to_end, num_choices, iter_idx, lhs, rhs):
            if ch_pos_to_end > len(result):
                return True

            mul = pow(10, ch_pos_to_end - 1)
            if iter_idx < len(words):
                word = words[iter_idx]
                idx = len(word) - ch_pos_to_end
                if idx >= 0:
                    if word[idx] not in num_mappings:
                        for n in num_choices:
                            if n == 0 and word[idx] == word[0]:
                                continue
                            num_mappings[word[idx]] = n
                            if backtrack(ch_pos_to_end, num_choices - {n}, iter_idx + 1,
                                         lhs + num_mappings[word[idx]] * mul,
                                         rhs):
                                return True
                            del num_mappings[word[idx]]
                    else:
                        return backtrack(ch_pos_to_end, num_choices, iter_idx + 1, lhs + num_mappings[word[idx]] * mul, rhs)
                else:
                    return backtrack(ch_pos_to_end, num_choices, iter_idx + 1, lhs, rhs)
            elif iter_idx == len(words):
                idx = len(result) - ch_pos_to_end
                if result[idx] not in num_mappings:
                    for n in num_choices:
                        if n == 0 and result[idx] == result[0]:
                            continue
                        new_rhs = rhs + n * mul
                        if not str(lhs).endswith(str(new_rhs)):
                            continue
                        num_mappings[result[idx]] = n
                        if backtrack(ch_pos_to_end + 1, num_choices - {n}, 0, lhs, new_rhs):
                            return True
                        del num_mappings[result[idx]]
                else:
                    added = num_mappings[result[idx]]
                    if not str(lhs).endswith(str(rhs + added * mul)):
                        return False
                    return backtrack(ch_pos_to_end + 1, num_choices, 0, lhs, rhs + added * mul)
            return False

        max_len_words = max([len(w) for w in words])
        if max_len_words > len(result):
            return False
        num_mappings = {}
        nums = {9, 8, 7, 6, 5, 4, 3, 2, 1, 0}
        return backtrack(1, nums, 0, 0, 0)

class Solution(object):
    def isSolvable(self, words, result):
        words.append(result)
        R, C = len(words), max(map(len, words))

        assigned = {}
        assigned_inv = [None] * 10

        def search(column, row, bal):
            if column >= C:
                return bal == 0
            if row == R:
                return bal % 10 == 0 and search(column + 1, 0, bal // 10)

            word = words[row]
            if column >= len(word):
                return search(column, row + 1, bal)

            letter = word[~column]
            sign = 1 if row < R - 1 else -1
            if letter in assigned:
                if (assigned[letter] or len(word) == 1 or column != len(word) - 1):
                    return search(column, row + 1, bal + sign * assigned[letter])
                return False
            else:
                for d, ad in enumerate(assigned_inv):
                    if ad is None and (d or len(word) == 1 or column != len(word) - 1):
                        assigned_inv[d] = letter
                        assigned[letter] = d
                        if search(column, row + 1, bal + sign * d):
                            return True
                        assigned_inv[d] = None
                        del assigned[letter]

            return False

        return search(0, 0, 0)

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        # backtracking?
        # awice ++
        words.append(result)
        R, C = len(words), max(list(map(len, words)))
        used = {}
        used_d = [None] * 10
        
        def backtrack(row, col, bal):
            if col >= C:
                return bal == 0 and all(used[w[0]] != 0 for w in words)
            if row == R:
                return bal % 10 == 0 and backtrack(0, col + 1, bal // 10)
            word = words[row]
            if col >= len(word):
                return backtrack(row + 1, col, bal)
            
            letter = word[-1 - col]
            sign = 1 if row < R - 1 else -1
            if letter in used:
                return backtrack(row + 1, col, bal + sign * used[letter])
            else:
                for d, ad in enumerate(used_d):
                    if ad is None and (d or col != len(word) - 1):
                        # start backtracking
                        used[letter] = d
                        used_d[d] = letter
                        if backtrack(row + 1, col, bal + sign * d):
                            return True
                        # restore to previous state
                        used_d[d] = None
                        del used[letter]
                        
            return False
        
        return backtrack(0, 0, 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
        equations = [[result[-i-1]] + [word[-i-1] for word in words if i<len(word)] for i in range(max_len)]
        used_digits = set()
        nonzero_chars = set(word[0] for word in words + [result])
        assignments = {}
        print(equations)
        def isSAT(eqn_index, carry):
            if eqn_index >= max_len:
                return carry == 0
            remaining_terms = []
            for t in equations[eqn_index]:
                if t not in assignments:
                    for guess in range(t in nonzero_chars, 10):
                        if guess in used_digits:
                            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
            return isSAT(eqn_index +1, s // 10)
           
        return isSAT(0, 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
        equations = [[result[-i-1]] + [word[-i-1] for word in words if i<len(word)] for i in range(max_len)]
        used_digits = set()
        nonzero_chars = set(word[0] for word in words + [result])
        assignments = {}
        def isSAT(eqn_index, carry):
            if eqn_index >= max_len:
                return carry == 0
            remaining_terms = []
            for t in equations[eqn_index]:
                if t not in assignments:
                    for guess in range(t in nonzero_chars, 10):
                        if guess in used_digits:
                            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
            return isSAT(eqn_index +1, s // 10)
           
        return isSAT(0, 0)

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        words.append(result)
        assigned = {}
        assigned_inv = [None] * 10
        self.r,self.c=len(words),max(list(map(len, words)))
        
        def dfs(column,row,bal):
            if column>=self.c:
                return bal==0 and all(assigned[i[0]]!=0 for i in words)
            if row==self.r:
                return bal%10==0 and dfs(column+1,0,bal//10)
            
            word=words[row]
            if column>=len(word):
                return dfs(column,row+1,bal)
            letter=word[~column]
            sign= 1 if row<self.r-1 else -1
            if letter in assigned:
                return dfs(column,row+1,bal+sign*assigned[letter])
            else:
                for num,c in enumerate(assigned_inv):
                    if c is None and (num or column!=len(word)-1):
                        assigned[letter]=num
                        assigned_inv[num]=letter
                        if dfs(column,row+1,bal+sign*num):
                            return True
                        assigned_inv[num]=None
                        del assigned[letter]
            return False
            
        return dfs(0,0,0)
                        
            
        
        
        


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        words.append(result)
        assigned = {}
        assigned_inv = [None] * 10
        self.r,self.c=len(words),max(list(map(len, words)))
        
        def dfs(column,row,bal):
            if column==self.c:
                return bal==0 and all(assigned[i[0]]!=0 for i in words)
            if row==self.r:
                return bal%10==0 and dfs(column+1,0,bal//10)
            
            word=words[row]
            if column>=len(word):
                return dfs(column,row+1,bal)
            letter=word[~column]
            sign= 1 if row<self.r-1 else -1
            if letter in assigned:
                return dfs(column,row+1,bal+sign*assigned[letter])
            else:
                for num,c in enumerate(assigned_inv):
                    if c is None and (num or column!=len(word)-1):
                        assigned[letter]=num
                        assigned_inv[num]=letter
                        if dfs(column,row+1,bal+sign*num):
                            return True
                        assigned_inv[num]=None
                        del assigned[letter]
            return False
            
        return dfs(0,0,0)
                        
            
        
        
        


class Solution:

    def isSolvable(self, words: List[str], result: str) -> bool:
        def solve(i, j, carry):
            # The current column assignment is over, so check for validity
            if j == len(words): 
                csum = carry
                for k in range(len(words)):
                    csum += 0 if i >= len(words[k]) else assign[words[k][i]] 
                # We have come to column i, but the result itself is not long enough.    
                if i >= len(result): return False 
                if result[i] in assign:
                    return csum % 10 == assign[result[i]] and solve(i+1, 0, csum // 10) # i th char of result  is already assigned, so check if its valid and go to next column i+1 and start from word 0
                else:
                    # If the current digit can't be assigned to ith char of result or if its 0 and we are looking at first char of a word: then return False
                    if (csum % 10) in assign.values() or (csum % 10 == 0 and i == len(result) - 1):
                        return False
                    assign[result[i]] = csum % 10
                    ret = solve(i+1, 0, csum // 10)
                    del assign[result[i]]
                    return ret
                
            if i == len(result): 
                return i >= max(len(w) for w in words)  and carry == 0 and all(assign[w[len(w)-1]] != 0 for w in words + [result])
            # Handle length of word less than the column we are looking at OR the ith column char of the jth word is already assigned previously
            if i >= len(words[j]) or words[j][i] in assign: return solve(i, j+1, carry)     
            for val in range(10):
                if val == 0 and i == len(words[j]) - 1: continue  # Handle not to assign 0 for first letter of a word 
                if val not in assign.values():
                    assign[words[j][i]] = val
                    ret = solve(i, j+1, carry)
                    if ret: return True
                    del assign[words[j][i]]   
            return False
        
        result = result[::-1]
        words = [w[::-1] for w in words]
        assign = dict()
        return solve(0, 0, 0)

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        n = len(words)
        mapper = {}
        maxlen = 0
        for w in words:
            maxlen = max(maxlen, len(w))
            for c in w:
                mapper[c] = -1
        if len(result) < maxlen or len(result) - maxlen > 1:
            return False
        for c in result:
            mapper[c] = -1
        used = [0] * 10
        def solve(i, j, s):
            if j == n:
                l = len(result) - i
                if l < 0:
                    if s != 0:
                        return False
                    for w in words:
                        if mapper[w[0]] == 0:
                            return False
                    if mapper[result[0]] == 0:
                        return False
                    return True
                c, s = divmod(s, 10)
                if mapper[result[l]] >= 0:
                    if mapper[result[l]] == s:
                        return solve(i + 1, 0, c)
                    return False
                if used[s]:
                    return False
                mapper[result[l]] = s
                used[s] = 1
                res = solve(i + 1, 0, c)
                mapper[result[l]] = -1
                used[s] = 0
                return res
            w = words[j]
            l = len(w) - i
            if l < 0:
                return solve(i, j + 1, s)
            if mapper[w[l]] >= 0:
                return solve(i, j + 1, s + mapper[w[l]])
            for k in range(10):
                if used[k]:
                    continue
                used[k] = 1
                mapper[w[l]] = k
                if solve(i, j + 1, s + k):
                    return True
                used[k] = 0
                mapper[w[l]] = -1
            return False
        return solve(1, 0, 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(t in nonzero_chars, 10):
                        if guess in used_digits:
                            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)

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        allwords = words + [result]
        n = max(list(map(len, allwords)))
        firstc = set(word[0] for word in allwords)
        if len(result) < n : return False
        def dfs(charidx, wordidx, carry, visited, char2digit):
            if charidx == n: return carry == 0
            if wordidx == len(allwords):
                tot = sum(char2digit[word[~charidx]] if charidx < len(word) else 0 for word in words) + carry
                if (tot % 10) == char2digit[result[~charidx]]:
                    return dfs(charidx + 1, 0, tot // 10, visited, char2digit)
                else:
                    return False
            if  wordidx < len(words) and charidx >= len(words[wordidx]):
                return dfs(charidx, wordidx+1, carry, visited, char2digit)
            
            c = allwords[wordidx][~charidx]
            first = 1 if c in firstc else 0
            if c in char2digit:
                return dfs(charidx, wordidx+1, carry, visited, char2digit)
            else:
                for d in range(first, 10):
                    if d not in visited:
                        visited.add(d)
                        char2digit[c] = d
                        if dfs(charidx, wordidx+1, carry, visited, char2digit): return True
                        del char2digit[c]
                        visited.remove(d)
            return False
      
        return dfs(0, 0, 0, set(), {})
                    
             
                
            
            


from itertools import permutations, zip_longest
from collections import OrderedDict
class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        
        self.matched_chars = list(zip_longest(*[result[::-1]]+[w[::-1] for w in words]))        
        self.first_chars = set([result[0]]+[w[0] for w in words])
        self.chars = []            
        self.free_vars = []
        self.idx = {}
        observed = set()
        for chars in self.matched_chars:
            free_vars = []
            for c in chars:
                if c is None:
                    continue
                if c not in observed:
                    self.chars.append(c)
                    free_vars.append(c)
                    observed.add(c)
                    self.idx[c]=len(self.idx)
            self.free_vars.append(free_vars)
        #print(self.free_vars)
        #print(self.chars)    

        return self.dfs(0,(),0)
        
    def dfs(self, i, used_digits, carry):
        #pemutations
        if i >= len(self.matched_chars):
            #print('R:',used_digits)
            return not max(used_digits[self.idx[f]]==0 for f in self.first_chars)
        free_vars = self.free_vars[i]
        perms = permutations(set(range(10))-set(list(used_digits)),len(free_vars))
        for p in perms:
            values = tuple(list(used_digits)+list(p))
            #check for contradiction
            nxt_carry = self.contradict(values,i,carry)
            if nxt_carry<0:
                continue
            if self.dfs(i+1,values,nxt_carry):
                return True
        return False
    
    def contradict(self, values, i, carry):
        r, *i = self.matched_chars[i]
        s = sum(values[self.idx[d]] for d in i if d)+carry
        if (s-values[self.idx[r]])%10:
            return -1
        return s//10
        
    
        
        
    
        
    
                            
                    
        
        
        


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        allWords = words + [result]
        firstChars = set(word[0] for word in allWords if len(word) > 1)
        n = max(list(map(len, allWords)))
        if len(result) < n: return False
        def dfs(charIdx, wordIdx, carry, visited, char2digit):
            if charIdx == n: return carry == 0
            if wordIdx == len(allWords):
                # time to check the final status for the current digit
                sums = sum(char2digit[word[~charIdx]] if charIdx < len(word) else 0 for word in words) + carry
                if sums % 10 == char2digit[result[-charIdx - 1]]:
                    return dfs(charIdx + 1, 0, sums // 10, visited, char2digit)
                else:
                    return False # prune. To support this, using -charIdx - 1 to visit from right/low to left/high
            # current word length is too short to check, move to check next word
            if wordIdx < len(words) and charIdx >= len(words[wordIdx]):
                return dfs(charIdx, wordIdx + 1, carry, visited, char2digit)

            c = allWords[wordIdx][-charIdx-1]
            if c in char2digit:
                # if current word's current char already map to a digit, continue with next word
                return dfs(charIdx, wordIdx + 1, carry, visited, char2digit)
            else:
                # otherwise try all possibilities via dfs
                firstDigit = 1 if c in firstChars else 0
                for digit in range(firstDigit, 10):
                    if digit not in visited:
                        visited.add(digit)
                        char2digit[c] = digit
                        if dfs(charIdx, wordIdx + 1, carry, visited, char2digit): return True
                        del char2digit[c]
                        visited.remove(digit) # restore visited and char2digit by discarding the copy
                return False
        return dfs(0, 0, 0, set(), {})
            


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        n = len(words)
        mapper = {}
        maxlen = 0
        for w in words:
            maxlen = max(maxlen, len(w))
            for c in w:
                mapper[c] = -1
        if len(result) < maxlen or len(result) - maxlen > 1:
            return False
        for c in result:
            mapper[c] = -1
        used = [0] * 10
        def solve(i, j, s):
            if j == n:
                l = len(result) - i
                if l < 0:
                    if s != 0:
                        return False
                    if any([mapper[w[0]] == 0 for w in words]):
                        return False
                    if mapper[result[0]] == 0:
                        return False
                    return True
                c, s = divmod(s, 10)
                if mapper[result[l]] >= 0:
                    if mapper[result[l]] == s:
                        return solve(i + 1, 0, c)
                    return False
                if used[s]:
                    return False
                mapper[result[l]] = s
                used[s] = 1
                res = solve(i + 1, 0, c)
                mapper[result[l]] = -1
                used[s] = 0
                return res
            w = words[j]
            l = len(w) - i
            if l < 0:
                return solve(i, j + 1, s)
            if mapper[w[l]] >= 0:
                return solve(i, j + 1, s + mapper[w[l]])
            for k in range(10):
                if used[k]:
                    continue
                used[k] = 1
                mapper[w[l]] = k
                if solve(i, j + 1, s + k):
                    return True
                used[k] = 0
                mapper[w[l]] = -1
            return False
        return solve(1, 0, 0)

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        allwords = words + [result]
        n = max(list(map(len, allwords)))
        firstc = set(word[0] for word in allwords)
        if len(result) < n : return False
        def dfs(charidx, wordidx, carry, visited, char2digit):
            if charidx == n: return carry == 0
            if wordidx == len(allwords):
                tot = sum(char2digit[word[~charidx]] if charidx < len(word) else 0 for word in words) + carry
                if (tot % 10) == char2digit[result[~charidx]]:
                    return dfs(charidx + 1, 0, tot // 10, visited, char2digit)
                return False
            if  wordidx < len(words) and charidx >= len(words[wordidx]):
                return dfs(charidx, wordidx+1, carry, visited, char2digit)
            
            c = allwords[wordidx][~charidx]
            first = 1 if c in firstc else 0
            if c in char2digit:
                return dfs(charidx, wordidx+1, carry, visited, char2digit)
            for d in range(first, 10):
                if d not in visited:
                    visited.add(d)
                    char2digit[c] = d
                    if dfs(charidx, wordidx+1, carry, visited, char2digit): return True
                    del char2digit[c]
                    visited.remove(d)
            return False
      
        return dfs(0, 0, 0, set(), {})
                    
             
                
            
            


from itertools import permutations, zip_longest
from collections import OrderedDict
class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        
        self.matched_chars = list(zip_longest(*[result[::-1]]+[w[::-1] for w in words]))        
        self.first_chars = set([result[0]]+[w[0] for w in words])
        self.chars = []            
        self.free_vars = []
        self.idx = {}
        observed = set()
        for chars in self.matched_chars:
            free_vars = []
            for c in chars:
                if c is None:
                    continue
                if c not in observed:
                    self.chars.append(c)
                    free_vars.append(c)
                    observed.add(c)
                    self.idx[c]=len(self.idx)
            self.free_vars.append(free_vars)
        #print(self.free_vars)
        #print(self.chars)    

        return self.dfs(0,(),0)
        
    #@lru_cache(maxsize=None)
    def dfs(self, i, used_digits, carry):
        #pemutations
        if i >= len(self.matched_chars):
            #print('R:',used_digits)
            return not max(used_digits[self.idx[f]]==0 for f in self.first_chars)
        free_vars = self.free_vars[i]
        perms = permutations(set(range(10))-set(list(used_digits)),len(free_vars))
        for p in perms:
            values = tuple(list(used_digits)+list(p))
            #check for contradiction
            nxt_carry = self.contradict(values,i,carry)
            if nxt_carry<0:
                continue
            if self.dfs(i+1,values,nxt_carry):
                return True
        return False
    
    def contradict(self, values, i, carry):
        r, *i = self.matched_chars[i]
        s = sum(values[self.idx[d]] for d in i if d)+carry
        if (s-values[self.idx[r]])%10:
            return -1
        return s//10
        
    
        
        
    
        
    
                            
                    
        
        
        


# 1307. Verbal Arithmetic Puzzle
# version 2

def make_zip (lists):
    i = 0
    maxlength = max (len (l) for l in lists)
    ans = []
    while i < maxlength:
        ans.append ([l[i] for l in lists if i < len (l)])
        i += 1
    return ans

def make_order (words, result):
    order = []
    formulas = {}
    for i in range (len (result)):
        for ch in [*(words[i]), result[i]]:
            if ch not in order:
                order.append (ch)
        order.append (f'c{i+1}')
        lhs = words[i]
        rhs = result[i]
        if i > 0:
            lhs.append (f'c{i}')
        excess = f'c{i+1}'
        formulas[excess] = (lhs, rhs, excess)
    # order determined
    return order, formulas

def find_free (repl, ch, nonzero):
    start = 1 if ch in nonzero else 0
    choices = set (range (start, 10))
    for x, y in repl.items ():
        if y in choices: choices.remove (y)
    yield from choices

def find_value (n, repl, crepl):
    return repl[n] if n in repl else crepl[n]

def find_excess (lhs, rhs, repl, crepl):
    return sum (find_value (x, repl, crepl) for x in lhs) - find_value (rhs, repl, crepl)

def walk_solutions (puzzle, index, repl, crepl):
    (words, result, order, formulas, nonzero) = puzzle

    if index == len (order):
        # check top digit zero
        last_ch = order[-1]
        if crepl[last_ch] != 0:
            return
        yield repl
    else:
        ch = order[index]
        if len (ch) == 1:
            for digit in find_free (repl, ch, nonzero):
                repl[ch] = digit
                yield from walk_solutions (puzzle, index + 1, repl, crepl)
                del repl[ch]
        else:
            formula = formulas[ch]
            (lhs, rhs, _) = formula
            excess = find_excess (lhs, rhs, repl, crepl)
            if excess >= 0 and excess % 10 == 0:
                # successful
                crepl[ch] = excess // 10
                yield from walk_solutions (puzzle, index + 1, repl, crepl)
                del crepl[ch]

def is_solvable (words, result):
    n = len (words)
    maxword = 10 ** max (len (w) for w in words) - 1
    minresult = 10 ** (len (result) - 1)
    if n * maxword < minresult:
        return False

    if not all (len (w) <= len (result) for w in words):
        return False

    nonzero = {m[0] for m in [*words, result] if len (m) > 1}

    result = [ch for ch in result[::-1]]
    words = make_zip ([w[::-1] for w in words])
    while len (words) < len (result):
        words.append ([])

    order, formulas = make_order (words, result)

    puzzle = (words, result, order, formulas, nonzero)

    return any (walk_solutions (puzzle, 0, {}, {}))

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        return is_solvable(words, result)

from itertools import permutations, zip_longest
from collections import OrderedDict
class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        
        self.matched_chars = list(zip_longest(*[result[::-1]]+[w[::-1] for w in words]))        
        self.first_chars = set([result[0]]+[w[0] for w in words])
        self.chars = []            
        self.free_vars = []
        self.idx = {}
        observed = set()
        for chars in self.matched_chars:
            free_vars = []
            for c in chars:
                if c is None:
                    continue
                if c not in observed:
                    self.chars.append(c)
                    free_vars.append(c)
                    observed.add(c)
                    self.idx[c]=len(self.idx)
            self.free_vars.append(free_vars)
        #print(self.free_vars)
        #print(self.chars)    

        return self.dfs(0,(),0)
        
    @lru_cache(maxsize=None)
    def dfs(self, i, used_digits, carry):
        #pemutations
        if i >= len(self.matched_chars):
            #print('R:',used_digits)
            return not max(used_digits[self.idx[f]]==0 for f in self.first_chars)
        free_vars = self.free_vars[i]
        perms = permutations(set(range(10))-set(list(used_digits)),len(free_vars))
        for p in perms:
            values = tuple(list(used_digits)+list(p))
            #check for contradiction
            nxt_carry = self.contradict(values,i,carry)
            if nxt_carry<0:
                continue
            if self.dfs(i+1,values,nxt_carry):
                return True
        return False
    
    def contradict(self, values, i, carry):
        r, *i = self.matched_chars[i]
        s = sum(values[self.idx[d]] for d in i if d)+carry
        if (s-values[self.idx[r]])%10:
            return -1
        return s//10
        
    
        
        
    
        
    
                            
                    
        
        
        


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        allWords = words + [result]
        firstChars = set(word[0] for word in allWords if len(word) > 1)
        n = max(list(map(len, allWords)))
        if len(result) < n: return False
        def dfs(charIdx, wordIdx, carry, visited, char2digit):
            if charIdx == n: return carry == 0
            if wordIdx == len(allWords):
                # time to check the final status for the current digit
                sums = sum(char2digit[word[~charIdx]] if charIdx < len(word) else 0 for word in words) + carry
                if sums % 10 == char2digit[result[-charIdx - 1]]:
                    return dfs(charIdx + 1, 0, sums // 10, visited, char2digit)
                else:
                    return False # prune. To support this, using -charIdx - 1 to visit from right/low to left/high
            # current word length is too short to check, move to check next word
            if wordIdx < len(words) and charIdx >= len(words[wordIdx]):
                return dfs(charIdx, wordIdx + 1, carry, visited, char2digit)

            c = allWords[wordIdx][-charIdx-1]
            if c in char2digit:
                # if current word's current char already map to a digit, continue with next word
                return dfs(charIdx, wordIdx + 1, carry, visited, char2digit)
            else:
                # otherwise try all possibilities via dfs
                firstDigit = 1 if c in firstChars else 0
                for digit in range(firstDigit, 10):
                    if digit not in visited:
                        visited.add(digit)
                        char2digit[c] = digit
                        if dfs(charIdx, wordIdx + 1, carry, visited, char2digit.copy()): return True
                        visited.remove(digit) # restore visited and char2digit by discarding the copy
                return False
        return dfs(0, 0, 0, set(), {})
            


from itertools import permutations, zip_longest
from collections import OrderedDict
class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        
        self.matched_chars = list(zip_longest(*[result[::-1]]+[w[::-1] for w in words]))        
        self.first_chars = set([result[0]]+[w[0] for w in words])
        self.chars = []            
        self.free_vars = []
        self.idx = {}
        observed = set()
        for chars in self.matched_chars:
            free_vars = []
            for c in chars:
                if c is None:
                    continue
                if c not in observed:
                    self.chars.append(c)
                    free_vars.append(c)
                    observed.add(c)
                    self.idx[c]=len(self.idx)
            self.free_vars.append(free_vars)
        print((self.free_vars))
        print((self.chars))    

        return self.dfs(0,(),0)
        
    @lru_cache(maxsize=None)
    def dfs(self, i, used_digits, carry):
        #pemutations
        if i >= len(self.matched_chars):
            print(('R:',used_digits))
            return not max(used_digits[self.idx[f]]==0 for f in self.first_chars)
        free_vars = self.free_vars[i]
        perms = permutations(set(range(10))-set(list(used_digits)),len(free_vars))
        for p in perms:
            values = tuple(list(used_digits)+list(p))
            #check for contradiction
            nxt_carry = self.contradict(values,i,carry)
            if nxt_carry<0:
                continue
            if self.dfs(i+1,values,nxt_carry):
                return True
        return False
    
    def contradict(self, values, i, carry):
        r, *i = self.matched_chars[i]
        s = sum(values[self.idx[d]] for d in i if d)+carry
        if (s-values[self.idx[r]])%10:
            return -1
        return s//10
        
    
        
        
    
        
    
                            
                    
        
        
        


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        allWords = words + [result]
        firstChars = set(word[0] for word in allWords if len(word) > 1)
        n = max(list(map(len, allWords)))
        if len(result) < n: return False
        def dfs(charIdx, wordIdx, carry, visited, char2digit):
            if charIdx == n: return carry == 0
            if wordIdx == len(allWords):
                # time to check the final status for the current digit
                sums = sum(char2digit[word[-charIdx - 1]] if charIdx < len(word) else 0 for word in words) + carry
                if sums % 10 == char2digit[result[-charIdx - 1]]:
                    return dfs(charIdx + 1, 0, sums // 10, visited, char2digit)
                else:
                    return False # prune. To support this, using -charIdx - 1 to visit from right/low to left/high
            # current word length is too short to check, move to check next word
            if wordIdx < len(words) and charIdx >= len(words[wordIdx]):
                return dfs(charIdx, wordIdx + 1, carry, visited, char2digit)

            c = allWords[wordIdx][-charIdx-1]
            if c in char2digit:
                # if current word's current char already map to a digit, continue with next word
                return dfs(charIdx, wordIdx + 1, carry, visited, char2digit)
            else:
                # otherwise try all possibilities via dfs
                firstDigit = 1 if c in firstChars else 0
                for digit in range(firstDigit, 10):
                    if digit not in visited:
                        visited.add(digit)
                        char2digit[c] = digit
                        if dfs(charIdx, wordIdx + 1, carry, visited, char2digit.copy()): return True
                        visited.remove(digit) # restore visited and char2digit by discarding the copy
                return False
        return dfs(0, 0, 0, set(), {})
            


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        n = len(words)
        mapper = {}
        maxlen = 0
        for w in words:
            maxlen = max(maxlen, len(w))
            for c in w:
                mapper[c] = -1
        if len(result) < maxlen or len(result) - maxlen > 1:
            return False
        for c in result:
            mapper[c] = -1
        used = [0] * 10
        def solve(i, j, s):
            if j == n:
                l = len(result) - i
                if l < 0:
                    if s != 0:
                        return False
                    if any(mapper[w[0]] == 0 for w in words):
                        return False
                    if mapper[result[0]] == 0:
                        return False
                    return True
                c, s = divmod(s, 10)
                if mapper[result[l]] >= 0:
                    if mapper[result[l]] == s:
                        return solve(i + 1, 0, c)
                    return False
                if used[s]:
                    return False
                mapper[result[l]] = s
                used[s] = 1
                res = solve(i + 1, 0, c)
                mapper[result[l]] = -1
                used[s] = 0
                return res
            w = words[j]
            l = len(w) - i
            if l < 0:
                return solve(i, j + 1, s)
            if mapper[w[l]] >= 0:
                return solve(i, j + 1, s + mapper[w[l]])
            for k in range(10):
                if used[k]:
                    continue
                used[k] = 1
                mapper[w[l]] = k
                if solve(i, j + 1, s + k):
                    return True
                used[k] = 0
                mapper[w[l]] = -1
            return False
        return solve(1, 0, 0)

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        allwords = words + [result]
        n = max(list(map(len, allwords)))
        firstc = set(word[0] for word in allwords)
        def dfs(charidx, wordidx, carry, visited, char2digit):
            if charidx == n: return carry == 0
            if wordidx == len(allwords):
                tot = sum(char2digit[word[~charidx]] if charidx < len(word) else 0 for word in words) + carry
                if tot % 10 == char2digit[result[~charidx]]:
                    return dfs(charidx+1, 0, tot//10, visited, char2digit)
                return False
            if wordidx < len(words) and charidx >= len(words[wordidx]):
                return dfs(charidx, wordidx+1, carry, visited, char2digit)
            c = allwords[wordidx][~charidx]
            if c in char2digit:
                return dfs(charidx, wordidx+1, carry, visited, char2digit)
            first = 1 if c in firstc else 0
            for d in range(first, 10):
                if d not in visited:
                    visited.add(d)
                    char2digit[c] = d
                    if dfs(charidx, wordidx+1, carry, visited, char2digit): return True
                    del char2digit[c]
                    visited.remove(d)
            return False
                    
                
                    
                    
        return dfs(0, 0, 0, set(), {})
                    
             
                
            
            


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        allWords = words + [result]
        firstChars = set(word[0] for word in allWords if len(word) > 1)
        n = max(map(len, allWords))

        if len(result) < n:
            return False

        def dfs(charIdx, wordIdx, carry, visited, char2digit):
            if charIdx == n:
                return carry == 0

            if wordIdx == len(allWords):
                # time to check the final status for the current digit
                sums = sum(char2digit[word[-charIdx - 1]] if charIdx < len(word) else 0 for word in words) + carry
                if sums % 10 == char2digit[result[-charIdx - 1]]:
                    return dfs(charIdx + 1, 0, sums // 10, visited, char2digit)
                else:
                    return False # prune. To support this, using -charIdx - 1 to visit from right/low to left/high

            # current word length is too short to check, move to check next word
            if wordIdx < len(words) and charIdx >= len(words[wordIdx]):
                return dfs(charIdx, wordIdx + 1, carry, visited, char2digit)

            # 从后向前枚举，这样可以方便检测进而早点剪枝
            c = allWords[wordIdx][-charIdx-1]
            if c in char2digit:
                # if current word's current char already map to a digit, continue with next word
                return dfs(charIdx, wordIdx + 1, carry, visited, char2digit)
            else:
                # otherwise try all possibilities via dfs
                firstDigit = 1 if c in firstChars else 0
                for digit in range(firstDigit, 10):
                    if digit not in visited:
                        visited.add(digit)
                        char2digit[c] = digit
                        if dfs(charIdx, wordIdx + 1, carry, visited, char2digit.copy()):
                            return True
                        visited.remove(digit) # restore visited and char2digit by discarding the copy
                return False
        return dfs(0, 0, 0, set(), {})

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        start = set()
        for word in words + [result]:
            if len(word) > 1:
                start.add(word[0])


        n = max(list(map(len, words + [result])))
        if len(result) < n:
            return False

        def dfs(idx, i, carry, visited, mp):
            if idx == n:
                return carry == 0
            if i == len(words) + 1:
                sums = sum(mp[word[-idx - 1]] if idx < len(word) else 0 for word in words) + carry
                if sums % 10 == mp[result[-idx - 1]]:
                    carry = sums // 10
                    return dfs(idx + 1, 0, carry, visited, mp)
                return False

            if (i < len(words) and idx >= len(words[i])):
                return dfs(idx, i + 1, carry, visited, mp)
            tmp = words + [result]
            ch = tmp[i][-idx-1]
            if ch in mp:
                return dfs(idx, i + 1, carry, visited, mp)
            begin = 0
            if ch in start:
                begin = 1
            for x in range(begin, 10):
                if x not in visited:
                    visited.add(x)
                    mp[ch] = x
                    if dfs(idx, i + 1, carry, visited, mp.copy()):
                        return True
                    visited.remove(x)
            return False

        return dfs(0, 0, 0, set(), {})
            


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        allwords = words + [result]
        n = max(list(map(len, allwords)))
        firstc = set(word[0] for word in allwords)
        def dfs(charidx, wordidx, carry, visited, char2digit):
            if charidx == n: return carry == 0
            if wordidx == len(allwords):
                tot = sum(char2digit[word[~charidx]] if charidx < len(word) else 0 for word in words) + carry
                if tot % 10 == char2digit[result[~charidx]]:
                    return dfs(charidx+1, 0, tot//10, visited, char2digit)
                return False
            if wordidx < len(words) and charidx >= len(words[wordidx]):
                return dfs(charidx, wordidx+1, carry, visited, char2digit)
            c = allwords[wordidx][~charidx]
            first = 1 if c in firstc else 0
            if c in char2digit:
                return dfs(charidx, wordidx+1, carry, visited, char2digit)
            for d in range(first, 10):
                if d not in visited:
                    visited.add(d)
                    char2digit[c] = d
                    if dfs(charidx, wordidx+1, carry, visited, char2digit): return True
                    del char2digit[c]
                    visited.remove(d)
            return False
                    
                
                    
                    
        return dfs(0, 0, 0, set(), {})
                    
             
                
            
            


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        ## https://leetcode.com/problems/verbal-arithmetic-puzzle/discuss/463921/python-backtracking-with-pruning-tricks
        ## from low digit position to high digit position, stop searching once (left side sum)%10 did not equal right side at current digit
        
        ## mark all initial characters, because not leading zeros are allowed. 
        start = set()
        for word in words + [result]:
            if len(word) > 1: ## note: a single 0 is allowed
                start.add(word[0])

        ## find the maximum length between all words and result
        n = max(list(map(len, words + [result])))
        if len(result) < n: ## if the length of result is shorter than other words, it's  not possible
            return False
        
        ## helper function:
        ## idx: the index currently processing (of words and result)
        ## i: i-th word in words; when i == len(words) + 1: we have processed all words + result at index 
        ## carry: the carry computed by summing all previous indexes of words
        def dfs(idx, i, carry, visited, mp):
            ## base case: when we reach the highest digit (most significant) position
            ## we should have carry == 0, otherwise the sums are not equal
            if idx == n: 
                return carry == 0
            ## when i == len(words) + 1: we have processed all words + result at index
            ## the specific index of word is word[-idx - 1]
            ## we check the sum added by carry
            ## if the sum does not match the digit at result[-idx - 1]
            ## return False
            if i == len(words) + 1:
                sums = sum(mp[word[-idx - 1]] if idx < len(word) else 0 for word in words) + carry
                if sums % 10 == mp[result[-idx - 1]]:
                    carry = sums // 10 ## update carry to the next index
                    ## recursive call to the next index and start from 0-th word
                    return dfs(idx + 1, 0, carry, visited, mp)
                return False 
            ## if current word (i-th) has shorter length than index, 
            ## skip it, it will be counted as 0 for this digit
            if (i < len(words) and idx >= len(words[i])):
                return dfs(idx, i + 1, carry, visited, mp)
            
            
            tmp = words + [result]
            ch = tmp[i][-idx-1] ## current character
            if ch in mp: ## if this character has been assigned a value
                return dfs(idx, i + 1, carry, visited, mp)
            
            ## backtrack: try every possible digit
            begin = 0
            if ch in start:
                begin = 1 ## if it is an initial character of some word
            for x in range(begin, 10):
                if x not in visited:
                    visited.add(x)
                    mp[ch] = x
                    if dfs(idx, i + 1, carry, visited, mp.copy()):
                        return True
                    visited.remove(x)
            return False
        return dfs(0, 0, 0, set(), {})
            
        


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        n = len(words)
        mapper = {}
        maxlen = 0
        for w in words:
            maxlen = max(maxlen, len(w))
            for c in w:
                mapper[c] = -1
        if len(result) < maxlen or len(result) - maxlen > 1:
            return False
        for c in result:
            mapper[c] = -1
        used = [0] * 10
        def solve(i, j, s):
            if j == n or i == len(result) + 1:
                l = len(result) - i
                if l < 0:
                    if s != 0:
                        return False
                    if any(mapper[w[0]] == 0 for w in words):
                        return False
                    if mapper[result[0]] == 0:
                        return False
                    return True
                c, s = divmod(s, 10)
                if mapper[result[l]] >= 0:
                    if mapper[result[l]] == s:
                        return solve(i + 1, 0, c)
                    return False
                if used[s]:
                    return False
                mapper[result[l]] = s
                used[s] = 1
                res = solve(i + 1, 0, c)
                mapper[result[l]] = -1
                used[s] = 0
                return res
            w = words[j]
            l = len(w) - i
            if l < 0:
                return solve(i, j + 1, s)
            if mapper[w[l]] >= 0:
                return solve(i, j + 1, s + mapper[w[l]])
            for k in range(10):
                if used[k]:
                    continue
                used[k] = 1
                mapper[w[l]] = k
                if solve(i, j + 1, s + k):
                    return True
                used[k] = 0
                mapper[w[l]] = -1
            return False
        return solve(1, 0, 0)

class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        start = set()
        for word in words + [result]:
            if len(word) > 1:
                start.add(word[0])


        n = max(map(len, words + [result]))
        if len(result) < n:
            return False

        def dfs(idx, i, carry, visited, mp):
            if idx == n:
                return carry == 0
            if i == len(words) + 1:
                sums = sum(mp[word[-idx - 1]] if idx < len(word) else 0 for word in words) + carry
                if sums % 10 == mp[result[-idx - 1]]:
                    carry = sums // 10
                    return dfs(idx + 1, 0, carry, visited, mp)
                return False

            if (i < len(words) and idx >= len(words[i])):
                return dfs(idx, i + 1, carry, visited, mp)
            tmp = words + [result]
            ch = tmp[i][-idx-1]
            if ch in mp:
                return dfs(idx, i + 1, carry, visited, mp)
            begin = 0
            if ch in start:
                begin = 1
            for x in range(begin, 10):
                if x not in visited:
                    visited.add(x)
                    mp[ch] = x
                    if dfs(idx, i + 1, carry, visited, mp.copy()):
                        return True
                    visited.remove(x)
            return False

        return dfs(0, 0, 0, set(), {})


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        start = set()
        for word in words + [result]:
            if len(word) > 1:
                start.add(word[0])


        n = max(map(len, words + [result]))
        if len(result) < n:
            return False

        def dfs(idx, i, carry, visited, mp):
            if idx == n:
                return carry == 0
            if i == len(words) + 1:
                sums = sum(mp[word[-idx - 1]] if idx < len(word) else 0 for word in words) + carry
                if sums % 10 == mp[result[-idx - 1]]:
                    carry = sums // 10
                    return dfs(idx + 1, 0, carry, visited, mp)
                return False

            if (i < len(words) and idx >= len(words[i])):
                return dfs(idx, i + 1, carry, visited, mp)
            tmp = words + [result]
            ch = tmp[i][-idx-1]
            if ch in mp:
                return dfs(idx, i + 1, carry, visited, mp)
            begin = 0
            if ch in start:
                begin = 1
            for x in range(begin, 10):
                if x not in visited:
                    visited.add(x)
                    mp[ch] = x
                    if dfs(idx, i + 1, carry, visited, mp.copy()):
                        return True
                    visited.remove(x)
            return False

        return dfs(0, 0, 0, set(), {})

from itertools import permutations

class Solution:
    digitMap = {}
    wordsRev = []
    resultRev = []
    limit = 0
    
    def findSolution(self, n, carry = 0):
        if n == self.limit:
            # Check leading zero policy
            leadingDigitChars = [w[len(w) - 1] for w in self.wordsRev]
            leadingDigitChars.append(self.resultRev[len(self.resultRev) - 1])
            leadingDigits = [self.digitMap[c] for c in leadingDigitChars]
            return 0 not in leadingDigits

        availableDigits = [n for n in range(0, 10) if n not in self.digitMap.values()]
        digitChars = [w[n] for w in self.wordsRev if n < len(w)]
        resultChar = self.resultRev[n]

        knownDigitChars = list(filter(lambda x: x in self.digitMap, digitChars))
        unknownDigitChars = [w for w in digitChars if w not in knownDigitChars]

        digits = []
        resultDigit = -1
        if len(knownDigitChars) > 0:
            digits = [self.digitMap[k] for k in knownDigitChars]
        if resultChar in self.digitMap:
            resultDigit = self.digitMap[resultChar]

        for d in permutations(availableDigits, len(unknownDigitChars)):
            s = sum(digits) + sum(d) + carry
            c = int(s / 10)
            s %= 10

            if resultDigit >= 0 and s == resultDigit:
                for i, v in enumerate(d):
                    self.digitMap[unknownDigitChars[i]] = v
                if self.findSolution(n+1, c):
                    return True
                else:
                    # Fallback
                    for i, v in enumerate(d):
                        if unknownDigitChars[i] in self.digitMap:
                            del self.digitMap[unknownDigitChars[i]]
            elif resultDigit < 0 and ((resultChar not in unknownDigitChars and s not in d) or (resultChar in unknownDigitChars and s in d)) and s in availableDigits:
                for i, v in enumerate(d):
                    self.digitMap[unknownDigitChars[i]] = v
                if resultChar not in unknownDigitChars:
                    self.digitMap[resultChar] = s
                elif s != self.digitMap[resultChar]:
                    for i, v in enumerate(d):
                        if unknownDigitChars[i] in self.digitMap:
                            del self.digitMap[unknownDigitChars[i]]
                    continue

                if self.findSolution(n+1, c):
                    return True
                else:
                    # Fallback
                    for i, v in enumerate(d):
                        if unknownDigitChars[i] in self.digitMap:
                            del self.digitMap[unknownDigitChars[i]]
                    if resultChar in self.digitMap:
                        del self.digitMap[resultChar]
        return False
            
    def isSolvable(self, words: List[str], result: str) -> bool:
        self.digitMap = {}
        self.wordsRev = [w[::-1] for w in words]
        self.resultRev = result[::-1]

        wordMax = max([len(w) for w in words])
        if wordMax > len(result):
            return False

        self.limit = max(wordMax, len(result))

        return self.findSolution(0, 0)

from collections import defaultdict
class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        def search(i: int, j: int, carry: int, used: int, ls: list, mp: defaultdict, non_zeros: set) -> bool:
            if j == len(ls[-1]):
                return carry == 0
            if i == len(ls):
                total = sum([mp[ls[r][j]] if j < len(ls[r]) else 0 for r in range(len(ls) - 1)]) + carry
                exp_total = mp[ls[-1][j]]
                if (total % 10) != exp_total:
                    return False
                return search(0, j + 1, total // 10, used, ls, mp, non_zeros)
            if j >= len(ls[i]) or ls[i][j] in mp:
                return search(i + 1, j, carry, used, ls, mp, non_zeros)
            start = 1 if ls[i][j] in non_zeros else 0
            for d in range(start, 10):
                if (1 << d) & used:
                    continue
                mp[ls[i][j]] = d
                if search(i + 1, j, carry, used | (1 << d), ls, mp, non_zeros):
                    mp.pop(ls[i][j])
                    return True
                mp.pop(ls[i][j])
            return False
        
        non_zeros = set([w[0] for w in words] + [result[0]])
        ls = [w[::-1] for w in words] + [result[::-1]]
        return search(0, 0, 0, 0, ls, defaultdict(int), non_zeros)

class Solution:
    
    def isSolvable(self, words: List[str], result: str) -> bool:
        
        allWords = words  + [result]
        firstChars = set(word[0] for word in allWords)
        maxWordLength = max(list(map(len, allWords)))
        
        if len(result) < maxWordLength: return False
        
        def dfs(charIdx, wordIdx, carry, visited, char2Digit):
            # check if the final sum is equal
            if charIdx == maxWordLength:
                return carry == 0
            
            # if we have assigned digits to all chars at the current index
            # check if the assigned values work
            if wordIdx == len(allWords):
                sums = sum(char2Digit[word[-charIdx-1]] if charIdx < len(word) else 0 for word in words)
                sums += carry
                if sums % 10 == char2Digit[result[-charIdx-1]]:
                    return dfs(charIdx + 1, 0, sums // 10, visited, char2Digit)
                else:
                    return False
            
            # if the current char index is longer than the current word, move to the next word
            currWord = allWords[-wordIdx-1]
            if charIdx >= len(currWord):
                return dfs(charIdx, wordIdx+1, carry, visited, char2Digit)
            
            # if we already have a digit assignment for the char, skip it
            currChar = currWord[-charIdx-1]
            if currChar in char2Digit:
                return dfs(charIdx, wordIdx+1, carry, visited, char2Digit)
            
            # otherwise try every possible digit
            else:
                startDigit = 1 if currChar in firstChars else 0
                for digit in range(startDigit, 10):
                    # skip previously assigned digits
                    if digit in list(char2Digit.values()): continue
                    # try the assignment
                    visited.add(digit)
                    char2Digit[currChar] = digit
                    if dfs(charIdx, wordIdx, carry, visited, char2Digit.copy()):
                        return True
                    visited.remove(digit)
                return False
        
        return dfs(0, 0, 0, set(), {})
                
            
            
        


class Solution:
    def isSolvable(self, words: List[str], result: str) -> bool:
        self.n = len(result)
        self.levels = []
        self.alldigit = {}
        self.allch = []
        self.result = result
        self.nonzero = set()
        for w in words:
            self.nonzero.add(w[0])
        self.nonzero.add(result[0])
 #       print(\"nonzero\", self.nonzero)
        for r in range(len(result)):
            l = []
            for w in words:
                if r < len(w):
                    l.append(w[len(w) - r - 1])
                
            l.append(result[len(result) - 1 - r])
            self.levels.append(l)
#        print(\"levels\", self.levels)
        self.occupy = set()
        self.checkdigit = {} # num of words to digit
        
        if len(self.levels[-1]) == 1:
            self.alldigit[self.levels[-1][0]] = 1
            self.occupy.add(1)
        
        for l in range(len(self.levels)):
            newch = set(self.levels[l]) - set(self.allch)
            self.allch.extend(newch)
            self.checkdigit[len(self.allch)] = l + 1
#        print(\"checkdigit\", self.checkdigit)
#        print(\"allch\", self.allch)
        if self.tryone(0, len(self.allch)):
#            print(self.alldigit)
            return True
        else:
#            print(self.alldigit)
            return False
        
    def tryone(self, level, maxl):
        flag = False
        if maxl == level:
            if self.check(self.checkdigit[level]):
#                print(\"final level\", self.alldigit)
                return True
            else:
                return False
        if level in self.checkdigit:
            if not self.check(self.checkdigit[level]):
                return False
            else:
                pass
#                if 'T' in self.alldigit and self.alldigit['T'] == 9 and level > 7:
#                    flag = True
#                    print(\"level:\", level, self.alldigit)
        
        if self.allch[level] in self.alldigit:
            if self.tryone(level + 1, maxl):
                return True
            else:
                return False
            
        for i in range(10):
            if i not in self.occupy:
                if i != 0 or self.allch[level] not in self.nonzero:
#                    if flag:
#                        print(\"level 8:\", level, i, self.allch[level])
                    self.occupy.add(i)
                    self.alldigit[self.allch[level]] = i
                    if self.tryone(level + 1, maxl):
                        return True
                    del self.alldigit[self.allch[level]]
                    self.occupy.remove(i)
        return False
        
        
    def check(self, level):
#        flag = False
#        if level > 5 and self.alldigit['I'] == 1 and self.alldigit['T'] >= 5:
#            flag = True
#            print(self.alldigit)
#        if self.alldigit['Y'] > 1 and self.alldigit['D'] > 6 and self.alldigit['E'] > 4:
#            flag = True
#            print(\"check level\", level, self.alldigit)
        plus = 0
#        if level == 5 and self.alldigit['F'] == 1 and self.alldigit['U'] == 9:
#            flag = True
#            print(\"digit:\", level, self.alldigit)
        for i in range(level):
            levelsum = 0
            for j in range(len(self.levels[i]) - 1):
                levelsum += self.alldigit[self.levels[i][j]]
#            if flag:
#                print(\"level, levelsum, plus, result\", level, levelsum, plus, self.alldigit[self.levels[i][-1]])
            if (levelsum + plus) % 10 != self.alldigit[self.levels[i][-1]]:
#                if flag:
#                    print(\"False\")
                return False
            else:
                plus = int((levelsum + plus)/10)
#                if flag:
#                    print(\"plus\", plus)
#        if flag:
#            print(\"True\")
        return True