Psuedo code for propagate on Kernel

propagate.pseudo

def apply(literal, assignment):
    if literal is a negation:
        return !assignment
    return assignment

def get_true_assignment(literal):
    if literal is a negation: 
        return False
    return True

def propagate(clauses):
    clauses_to_look_at = [1] * len(clauses)
    num_unary = 0
    WBH = 0
    lookahead_var = Some int
    lookahead_assignment = True/False
    assignment_trail[lookahead_var] = lookahead_assignment

    while num_unary == 0:
        num_unary = 1
        WBH = 0
        for clause in clauses:
            if ANY literal in clause => apply(assignment_trail[var(literal)]) is True:
                clauses_to_look_at[clause] = 0
                continue

            int active_literals = [] * NUM_LITERALS_PER_CLAUSE
            int active_literals_index = 0 
    
            for literal in clause:
                if apply(assignment_trail[var(literal})) is False:
                    active_literals -= 1;
                else:
                    active_literals[index] = literal
                    active_lierals_index += 1

            // two or more active literals are undefined
            if active_literals_index == 2:
                WBH = WBH + Weight[active_literals[0]] + Weight[active_literals[1]]

            // one literal in clause is undefined 
            if active_literals_index == 1:
                assignment_trail[var(literal)] = get_true_assignment
                num_unary = 0
                break

            // no literals are undefined -- all are false
            if active_literals_index == 0: 
                return -1 ( to be come UNSAT)