<p>Given an equation, represented by <code>words</code> on the left side and the <code>result</code> on the right side.</p>

<p>You need to check if the equation is solvable under the following rules:</p>

<ul>
	<li>Each character is decoded as one digit (0 - 9).</li>
	<li>No two characters can map to the same digit.</li>
	<li>Each <code>words[i]</code> and <code>result</code> are decoded as one number <strong>without</strong> leading zeros.</li>
	<li>Sum of numbers on the left side (<code>words</code>) will equal to the number on the right side (<code>result</code>).</li>
</ul>

<p>Return <code>true</code> <em>if the equation is solvable, otherwise return</em> <code>false</code>.</p>

<p>&nbsp;</p>
<p><strong class="example">Example 1:</strong></p>

<pre>
<strong>Input:</strong> words = [&quot;SEND&quot;,&quot;MORE&quot;], result = &quot;MONEY&quot;
<strong>Output:</strong> true
<strong>Explanation:</strong> Map &#39;S&#39;-&gt; 9, &#39;E&#39;-&gt;5, &#39;N&#39;-&gt;6, &#39;D&#39;-&gt;7, &#39;M&#39;-&gt;1, &#39;O&#39;-&gt;0, &#39;R&#39;-&gt;8, &#39;Y&#39;-&gt;&#39;2&#39;
Such that: &quot;SEND&quot; + &quot;MORE&quot; = &quot;MONEY&quot; ,  9567 + 1085 = 10652</pre>

<p><strong class="example">Example 2:</strong></p>

<pre>
<strong>Input:</strong> words = [&quot;SIX&quot;,&quot;SEVEN&quot;,&quot;SEVEN&quot;], result = &quot;TWENTY&quot;
<strong>Output:</strong> true
<strong>Explanation:</strong> Map &#39;S&#39;-&gt; 6, &#39;I&#39;-&gt;5, &#39;X&#39;-&gt;0, &#39;E&#39;-&gt;8, &#39;V&#39;-&gt;7, &#39;N&#39;-&gt;2, &#39;T&#39;-&gt;1, &#39;W&#39;-&gt;&#39;3&#39;, &#39;Y&#39;-&gt;4
Such that: &quot;SIX&quot; + &quot;SEVEN&quot; + &quot;SEVEN&quot; = &quot;TWENTY&quot; ,  650 + 68782 + 68782 = 138214</pre>

<p><strong class="example">Example 3:</strong></p>

<pre>
<strong>Input:</strong> words = [&quot;LEET&quot;,&quot;CODE&quot;], result = &quot;POINT&quot;
<strong>Output:</strong> false
<strong>Explanation:</strong> There is no possible mapping to satisfy the equation, so we return false.
Note that two different characters cannot map to the same digit.
</pre>

<p>&nbsp;</p>
<p><strong>Constraints:</strong></p>

<ul>
	<li><code>2 &lt;= words.length &lt;= 5</code></li>
	<li><code>1 &lt;= words[i].length, result.length &lt;= 7</code></li>
	<li><code>words[i], result</code> contain only uppercase English letters.</li>
	<li>The number of different characters used in the expression is at most <code>10</code>.</li>
</ul>

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

        @lru_cache(None)
        def bound(ind: int, numMap: int, up: bool) -> int:
            l, r, zero, res = 1, 9, -1, 0
            if not numMap&1:
                for j in range(ind, n):
                    if s[j] not in lead and ((coeff[s[j]] > 0) ^ up):
                        zero = j
                        break
            for j in range(ind, n):
                if j == zero:   continue
                if ((coeff[s[j]] > 0) ^ up):
                    while numMap&1<<l:   l += 1
                    res += coeff[s[j]]*l
                    l += 1
                else:
                    while numMap&1<<r:   r -= 1
                    res += coeff[s[j]]*r
                    r -= 1
            return res

        def backtrack(ind: int, numMap: int, ttl: int) -> bool:

            # Tight Prunning, find the lower bound and upper bound of the remaining letters and unassigned numbers
            if ttl < bound(ind, numMap, False) or ttl > bound(ind, numMap, True):  return False

            if ind == n:    return True

            for i in range(1 if s[ind] in lead else 0, 10):
                if not numMap & 1<<i:
                    if backtrack(ind+1, numMap|1<<i, ttl - i*coeff[s[ind]]):   return True
            return False

        coeff, mxLen, s, lead = defaultdict(int), 0, set(), set()
        for word in words:
            base = 1
            for c in word[::-1]:
                s.add(c)
                coeff[c] += base
                base *= 10
            if mxLen < len(word):   mxLen = len(word)
            if len(word) > 1:       lead.add(word[0])
        if mxLen > len(result) or mxLen < len(result)-1:  return False
        base = 1
        for c in result[::-1]:
            s.add(c)
            coeff[c] -= base
            base *= 10
        if len(result) > 1: lead.add(result[0])

        s, n = sorted(s, key=lambda c: abs(coeff[c]), reverse=True), len(s)

        return backtrack(0,0,0)
17200