This script finds a password of printable ASCII characters given a desired sum and product of the ASCII character codes in the password.

password_sum_and_product.py

#!/usr/bin/env python3
# pip install z3-solver
import z3

class OrdAt:
    '''
    Z3 has no way of arbitrarily getting a character at an index from a string.
    However, this problem requires us to get ASCII character codes from a
    string. When an object of this class is called, the return value is a
    BitVec with a number of bits that you specify; the 8 least significant bits
    are constrained to match the ASCII character code at the given position in
    the string.
    
    Some parts of this class were borrowed from this StackOverflow answer:
    https://stackoverflow.com/a/53785639/1149181
    '''
    def __init__(self, solver, bit_length):
        '''
        Arguments:
            solver:
                Pass the z3.Solver() that you are using. This is necessary for
                the 8 least significant bits of the return value when this
                object is called to be constrained to match the ASCII character
                code at the given position in the string.
            bit_length:
                The return value when this object is called will have this
                number of bits. This is useful if you need to add or multiply
                character codes but also need to avoid integer overflow. This
                can be less than 8, equal to 8, or greater than 8; just don't
                use a negative value or 0.
        '''
        self.solver = solver
        self.bit_length = bit_length
        self.ord_helper_counter = 0
    def __call__(self, s, i):
        '''
        Arguments:
            s:
                Pass the z3.String from which you want a BitVec whose 8 least
                significant bits are constrained to match the ASCII character
                code at the given position.
            i:
                The 8 least significant bits of the BitVec will be constrained
                to match the ASCII character code at this position within s.
        '''
        # Create a BitVec to represent the ASCII character code at position i
        # in the string. More bits allow the sum and product to reach greater
        # values without overflowing.
        v = z3.BitVec(
            "OrdAtHelper_{:d}_{:d}".format(i, self.ord_helper_counter),
            self.bit_length
        )
        self.ord_helper_counter += 1
        # However, only BitVec objects with 8 bits can be compared to
        # characters in a string. Truncate or extend the BitVec to 8 bits. This
        # gives us the 8 least significant bits.
        if self.bit_length < 8:
            v8 = z3.ZeroExt(8 - self.bit_length, v)
        elif self.bit_length > 8:
            v8 = z3.Extract(7, 0, v)
        else:
            v8 = v
        # Constrain the 8 least significant bits to match the character code in
        # the string.
        self.solver.add(z3.Unit(v8) == z3.SubString(s, i, 1))
        # Return the BitVec with all the bits, not just the 8 least
        # significant.
        return v
    def list_of_ord(self, s, len_s):
        '''
        This method quickly creates BitVec objects for all the positions within
        the string. This saves you from having to call __call__ for every
        character in the string yourself.
        
        Arguments:
            s:
                See the argument s in __call__.
            len_s:
                Pass the length of the string. Unlike Python strings, Z3
                strings do not know their lengths.
        '''
        return [self(s, i) for i in range(len_s)]

def find_password(sum_goal, product_goal, len_password):
    '''
    This function finds a password where:
    
    - The sum of the ASCII character codes is sum_goal.
    - The product of the ASCII character codes is product_goal.
    - The length of the password is len_password.
    
    The password is returned as a string of its AST representation (like repr).
    If no such password exists, then None is returned.
    
    Note that the order of the characters in the password may not match the
    actual password. That is because addition and multiplication are
    associative and commutative. You may want to run the result through an
    anagram solver.
    '''
    solver = z3.Solver()
    # We will solve for this password. Z3 requires that we fix its length.
    password = z3.String("password")
    solver.add(z3.Length(password) == len_password)
    # We will need to get ASCII character codes at arbitrary offsets in the
    # password. The sum and product will be truncated to 32 bits.
    password_as_list_of_ord = \
        OrdAt(solver, 32).list_of_ord(password, len_password)
    # Add the rules for the sum and product of the character codes.
    solver.add(z3.Sum(password_as_list_of_ord) == sum_goal)
    solver.add(z3.Product(password_as_list_of_ord) == product_goal)
    # Make sure that all the characters are printable.
    for cord in password_as_list_of_ord:
        solver.add(0x20 <= cord)
        solver.add(cord <= 0x7e)
    # Return the password if it was found.
    if solver.check() == z3.sat:
        # type(solver.model()[password]) is z3.SeqRef
        return solver.model()[password].as_string()
    return None

def main():
    password = find_password(640, 3661347039, 6)
    if password is None:
        print("The password was not found.")
    else:
        print("The password is:", password)

if __name__ == "__main__":
    main()