#!/usr/bin/env python3

'''Computes if a given horn formula is satisfiable or not.

Parameters:

- horn_formula, represents the horn formula. 

  It is a list of lists, in which each element of the list is a list
  of integers that represents a horn clause.  A positive integer
  represent a positive variable, a negative integer represent a
  negated variable.

  For example, the horn formula (X_1 v not(X_2) v not(X_3)) ^ (X_3 v not(X_2))
  is represented using the following list of lists [[1, -2, -3], [3, -2]].

- n, number of variables in the horn formula.

Returns:

- True, if the formula is satisfiable.

- False, otherwise.

'''

def horn_satisfiability(horn_formula, n):
    imp = []  # clauses with 1 positive variable
    neg = []  # clauses with only negated variables
    not_yet_satisfied_clause = []  # clauses in imp that are not yet satisfied

    # NegatedClauses[x] := {C | C is a clause and x appears negated in C}
    negated_instances_of_variable = [[] for _ in range(0, n + 1)]

    # ScoreClauses[i] := |{x | x appears negated in the i-th clause and assignment(x) = False}|
    clause_score = [0 for _ in range(0,  len(horn_formula))]

    # PositiveVariable[i] := {x | x appears positive in the i-th clause} (it's at most 1)
    positive_variable_of_clause = [0 for _ in range(0, len(horn_formula))]

    assignment = [False for _ in range(0, n + 1)]
    
    # Construct imp and neg
    for index, clause in enumerate(horn_formula):
        # Check if the clause has a positive variable
        found_positive_var = True if [x for x in clause if x > 0] != [] else False

        if not found_positive_var:
            neg.append(clause)
        else:
            imp.append(clause)

    # Set the correct score for each clause in IMP
    for index, clause in enumerate(imp):
        clause_score[index] = 0
        
        for x in clause:
            if x < 0:
                clause_score[index] += 1
                # memorize that x appears negated in this particular clause
                negated_instances_of_variable[-x].append(index)
            else:
                # memorize that x is the positive variable of the clause
                positive_variable_of_clause[index] = x

        if clause_score[index] == 0:
            not_yet_satisfied_clause.append(index)

    while not_yet_satisfied_clause:
        # get a clause that is not yet satisfied
        clause = not_yet_satisfied_clause.pop()
        # get its positive variable
        x = positive_variable_of_clause[clause]

        if not assignment[x]:
            # assign it to True
            assignment[x] = True
            
            # update the score of all the clauses in which x appears
            # as negated to check which clauses go from satisfied to
            # not satisfied
            for clause_index in negated_instances_of_variable[x]:
                clause_score[clause_index] -= 1
                if clause_score[clause_index] == 0:
                    not_yet_satisfied_clause.append(clause_index)

    # Check if every clause in NEG is satisfied
    for clause in neg:
        truth_value = any(assignment[abs(x)] for x in clause)
        if not truth_value:
            return False

    # If all goes well return the assignment
    return assignment[1:]