# Horn-SAT

Given a boolean formula consisting of Horn clauses, set a minimal number of variables to *True* in order to satisfy all clauses.

## A linear time algorithm

The algorithm starts by setting all variables to *False* and sets variables to *True* only if this choice is forced.

A clause is Horn if it contains at most one positive literal. Clauses that contain both a variable and its negation
can be safely ignored. To all other clauses a score is assigned, which is defined as the number of its negative literals that are still set to *False*. Clauses with a zero score that are not satisfied need their positive literal to be set to *True*.

Hence the algorithm simply consists of repeatedly selecting such an unsatisfied clause with zero score. If it has no positive literal then the formula can not be satisfied. Otherwise the variable appearing positively in the clause is set to *True* and the scores of the remaining unsatisfied clauses are updated. The procedures ends when all clauses are satisfied. Since the assignments to *True* where forced in the solution, the assignment is minimal as required.

The main difficulty is to maintain a data structure to permit all these operations to be done efficiently. For this purpose we have a `score`

table that associates to each clause its score and a reverse `pool`

table that associates to each score the set of corresponding clauses.

In addition we have for each variable a list `clauses_with_negvar`

of clauses where it appears negatively. Hence when setting a variable \(x\) to *True* we can decrease the score for each score where \(\neg x\) appears.

The following code solves this problem in linear time, as the work done for each literal per clause is constant.