How does this backtracking code ensure that the two strings don't have common elements?

I am trying this question on LeetCode:

Given a string s, find two disjoint palindromic subsequences of s such that the product of their lengths is maximized. The two subsequences are disjoint if they do not both pick a character at the same index. Return the maximum possible product of the lengths of the two palindromic subsequences. For e.g., if s = "leetcodecom", the output should be 9 (two strings are ete and cdc, etc.).

With some online help, I came up with the code below:

class Solution {
public:
    int res;
    
    bool isPalindrome(string& s) {
        int i=0, j=s.size()-1;
        while(i<j && s[i]==s[j]) {
            i++;
            j--;
        }
        return i>=j;
    }
    
    void helper(string& s, string& s1, string& s2, int start) {
        if(start>=s.size()) {
            if(isPalindrome(s1) and isPalindrome(s2)) {
                res=max((int)res, (int)s1.size()*(int)s2.size());
            }
            return;
        }

        s1+=s[start];
        helper(s, s1, s2, start+1);
        s1.pop_back();
        
        s2+=s[start];
        helper(s, s1, s2, start+1);
        s2.pop_back();
        
        helper(s, s1, s2, start+1);
    }
    
    int maxProduct(string s) {
        res=0;
        string s1, s2;
        helper(s, s1, s2, 0);
        
        return res;
    }
};

This works and gets ACed, but I am unsure how it ensures that the two strings are disjoint. I was expecting to have a check that would ensure this and update res iff the two strings are disjoint.

What gives?

Thanks!

The code ensures disjointness because the two recursive steop blocks in helper do not ever pull the same character into both s1 and s2.

Firstly, each call to helper will not return until processing the string until the end, including all the recursive cases which that triggers. Then the pop_back will return the respective sequence to its original value, at this level of recursion.

    s1+=s[start];
    helper(s, s1, s2, start+1);
    s1.pop_back();
    
    s2+=s[start];
    helper(s, s1, s2, start+1);
    s2.pop_back();

Whenever the first block finishes and control falls through to the second block, s1 is rewound back to the value it had on entry into this recursion level. Some of the same characters that were previously put into s1 get added to s2. But they never appear in both at the same time.

    helper(s, s1, s2, start+1);

This line advances the recursion to search for subsequences starting at all positions. But here, no characters are added to s1 or s2. Just the start index moves ahead. So again, since no characters are added, no common character can be added.

Throughout the recursion, s1 and s2 contain potentially interleaving subsequences of s, but no character from s ever appears in s1 and s2 at the same time.

This is hard to follow because it isn't functional recursion, due to the sequences being passed by reference and being destructively manipulated. It's a kind of iterative process that uses recursion to furnish it with a back-tracking stack; a push-down automaton, loosely speaking. It doesn't even return a value; its output is a side-effect on a member variable scoped outside of the recursion.

You have to intuit that the s2+=s[start]; and s2.pop_back() are balanced, paired stack-like operations, which bring the sequence to the same state, regardless of what went on in the recursion below (because the recursion below executed the same balanced push/pop pairs). Furthermore, the recursion below is always at start + 1, and moves only toward the right, so it will never add the same character to either subsequence. So we can see there is a local mutual exclusion in the same frame, plus mutual exclusion against the lower recursion frames.