def readSat(inString):
    """Convert a string representing a CNF formula into a Python data
    structure representing the same formula.

    Convert a string representing a CNF formula into a Python data
    structure representing the same formula. The parameter inString
    must describe a CNF formula in the ASCII format described in the
    textbook. The returned object is in our internal format for
    storing a (CNF) SAT formula: it is list of clauses, where each
    clause is a dictionary whose keys are variable names (stored as
    strings) and values are +1 for positive literals and -1 for
    negative literals.

    Args:

        inString (str): a CNF formula in the ASCII format described in
            the textbook

    Returns:
    
        list of dict: This is our internal format for storing a (CNF)
            SAT formula. It is list of clauses, where each clause is a
            dictionary whose keys are variable names (stored as
            strings) and values are +1 for positive literals, -1 for
            negative literals, and 0 if the variable appears in the
            same clause both positively and negatively.

    """

    clauseStrings = inString.split("AND")
    clauseStrings = [x.strip() for x in clauseStrings]

    # Here we deal with an annoying special case. Unfortunately, our
    # spec for SAT instances doesn't distinguish very nicely between
    # empty clauses (which are unsatisfiable by definition), and an
    # empty *set* of clauses (which is satisfiable by definition).
    # Let us agree that if after the above splitting and stripping,
    # clauseStrings contains a single element which is the empty
    # string, then we have an empty set of clauses. Any other result
    # is a nonempty set of clauses, one or more of which may in fact
    # be an empty clause.
    if len(clauseStrings) == 1 and clauseStrings[0] == "":
        clauseStrings = []

    clauseStrings = [x.strip("()") for x in clauseStrings]

    clauses = []
    for clauseString in clauseStrings:
        clause = dict()
        literals = clauseString.split("OR")
        literals = [x.strip() for x in literals]
        for literal in literals:
            if literal.startswith("NOT"):
                splitLiteral = literal.split()
                variableName = splitLiteral[1]
                if variableName not in clause:
                    clause[variableName] = -1
                elif clause[variableName] == 1:
                    clause[variableName] = 0
            elif len(literal) > 0:
                variableName = literal
                if variableName not in clause:
                    clause[variableName] = 1
                elif clause[variableName] == -1:
                    clause[variableName] = 0
        clauses.append(clause)

    return clauses