Horn satisfiability

Ideas:

* every clauses has a score that is defined as the number of negated
  variabiles that are still set to False. Use some kind of map/array
  to make the association clause -> score.

* for every variable we have a list of clauses in which it appears as
  negated. Therefore, after setting a variable to True, we then update
  the score of all the clauses in which it appears as negative.

* Which clauses are not satisfied ? Those whose score is 0. Therefore
  a list of some kind is necessary to keep track of the clauses which
  are not satisfied.

* How to represent a horn clause? Well, every variabile in the clause
  can be represented with an integer.  For example the inger 2
  corresponds to the variable X_2. For negated variables use the
  negative numbers.

  Example: (X_1 v not(X_2) v not(X_3)) is represented by the list of
  integers [1, -2, -3].
  
* How to represent a boolean formula comprised of only horn clauses ?
  Well, since we can represent every horn clause as a list, then a
  boolean formula can be represented as a list of lists.

Algorithm:

Input: List of lists corresponding to a boolean formula comprised of horn clauses
Output: An assignment of truth values to the variable present in the formula.

Begin
    0) Create 2 lists: a list IMP with clauses that contain at least 1 positive variable, and a list
       NEG with clauses that contain only negative variables.  O(n)
                
    1) Loop through each clause in IMP and set its score.
       If the score of the clause is 0, then add it to a list named UnsatisfiableClauses.
       Also, for each variable, create a list that contains the particular indexes of the clauses in
       which the variable is present as negated.
       For each clause memorize the only variable that is not negated. O(n)
       
    2) While UnsatisfiableClauses is not empty do
       2.1) Extract the first element l from UnsatisfiableClauses
       2.2) get the positive variable x in l
       2.3) assign x -> True
       2.4) Update (decrement) the score of all the clauses in which x appears as negated
            If the score of a clause reaches 0, then add the clause to the list UnsatisfiableClauses.

    3) Loop through every clause in NEG and check if there exist one clause that is not satisfied.
       In that case return None
       Otherwise return the assignment. O(n)