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.
def solve_horn_sat(formula):
# [...] build the data structure
# [...] this part is omitted
# --- solve Horn SAT formula
solution = set() # contains all variables set to True
while pool[0]:
curr = pool[0].pop() # arbitrary zero score clause
v = posvar_in_clause[curr]
if v == None: # formula is not satisfiable
return None
if v in solution or curr in clauses_with_negvar[v]:
continue # clause is already satisfied
solution.add(v)
for c in clauses_with_negvar[v]: # update score
pool[score[c]].remove(c)
score[c] -= 1
pool[score[c]].add(c) # change c to lower score in pool
return solution