Untitled

def branching_sat_solve(clause_set, partial_assignment=None, truth_assignment=None, backtrack_idx=-1, idx=-1):
    # Generate a truth assignment if it's not there
    if not truth_assignment:
        max_literal = -1
        # Extract all the literals, and set them initially to False.
        for clause in clause_set:
            abs_clause = list(map(lambda x: abs(x), clause))
            if max(abs_clause) > max_literal:
                max_literal = max(abs_clause)

        if partial_assignment:
            abs_partial_assignment = list(map(lambda x: abs(x), partial_assignment))
            truth_assignment = [-1 * num for num in range(1, max_literal + 1) if num not in abs_partial_assignment] + partial_assignment
            return branching_sat_solve(clause_set=clause_set, partial_assignment=partial_assignment, truth_assignment=truth_assignment, backtrack_idx=backtrack_idx, idx=idx)

        else:
            truth_assignment = [-1 * num for num in range(1, max_literal + 1)]
            return branching_sat_solve(clause_set=clause_set, partial_assignment=partial_assignment, truth_assignment=truth_assignment, backtrack_idx=backtrack_idx, idx=idx)

    # Check if the truth assignment satisfies the clause set
    else:
        num_valid_clauses = 0
        for clause in clause_set:
            valid_clause = False
            for literal in truth_assignment:
                if literal in clause:
                    valid_clause = True
                    break

            if valid_clause:
                num_valid_clauses += 1

        # Clause set is satisfied, return truth assignment
        if num_valid_clauses == len(clause_set):
            return truth_assignment

        # Backtrack, start at last index
        else:
            try:
                if backtrack_idx == idx:
                    if partial_assignment:
                        if truth_assignment[backtrack_idx] in partial_assignment:
                            return branching_sat_solve(clause_set=clause_set, partial_assignment=partial_assignment, truth_assignment=truth_assignment, backtrack_idx=backtrack_idx-1, idx=-1)

                        else:
                            if truth_assignment[backtrack_idx] < 0:
                                # Try negation of literal at backtrack idx
                                truth_assignment[backtrack_idx] = -1 * truth_assignment[backtrack_idx]

                                # Call func with backtrack_idx - 1, idx at the end
                                return branching_sat_solve(clause_set=clause_set, partial_assignment=partial_assignment,
                                                           truth_assignment=truth_assignment,
                                                           backtrack_idx=backtrack_idx - 1, idx=-1)

                            else:
                                truth_assignment[backtrack_idx] = -1 * truth_assignment[backtrack_idx]
                                return branching_sat_solve(clause_set=clause_set, partial_assignment=partial_assignment,
                                                           truth_assignment=truth_assignment,
                                                           backtrack_idx=backtrack_idx - 1, idx=-1)
                    else:
                        if truth_assignment[backtrack_idx] < 0:
                            # Try negation of literal at backtrack idx
                            truth_assignment[backtrack_idx] = -1 * truth_assignment[backtrack_idx]

                            # Call func with backtrack_idx - 1, idx at the end
                            return branching_sat_solve(clause_set=clause_set, partial_assignment=partial_assignment, truth_assignment=truth_assignment, backtrack_idx=backtrack_idx - 1, idx=-1)

                        else:
                            truth_assignment[backtrack_idx] = -1 * truth_assignment[backtrack_idx]
                            return branching_sat_solve(clause_set=clause_set, partial_assignment=partial_assignment, truth_assignment=truth_assignment, backtrack_idx=backtrack_idx - 1, idx=-1)

                else:
                    if partial_assignment:
                        # If the literal at truth_assignment[idx] is in the partial assignment, we skip past it.
                        if truth_assignment[idx] in partial_assignment:
                            return branching_sat_solve(clause_set=clause_set, partial_assignment=partial_assignment, truth_assignment=truth_assignment, backtrack_idx=backtrack_idx, idx=idx - 1)

                        else:
                            truth_assignment[idx] = -1 * truth_assignment[idx]
                            return branching_sat_solve(clause_set=clause_set, partial_assignment=partial_assignment,
                                                       truth_assignment=truth_assignment, backtrack_idx=backtrack_idx,
                                                       idx=idx - 1)

                    else:
                        truth_assignment[idx] = -1 * truth_assignment[idx]
                        return branching_sat_solve(clause_set=clause_set, partial_assignment=partial_assignment, truth_assignment=truth_assignment, backtrack_idx=backtrack_idx, idx=idx-1)

            except IndexError:
                return 'unsat'