# Source code for tryalgo.horn_sat

```#!/usr/bin/env python3
# -*- coding: utf-8 -*-
"""\
Solving Horn SAT

christoph dürr - 2016-2020

clauses are numbered starting from 0
variables are strings (identifier)

solution  : set of variables that are set to true
posvar_in_clause : maps clause to the unique positive variable in clause
(or None)
clause_with_negvar : maps variable v to all clauses that contain not(v)

every clause has a score: number of its negative variables
that are not in solution sol
pool : maps score to clauses of that score
"""

from collections import defaultdict
import sys

# To mock it, https://stackoverflow.com/a/44677646/827989

[docs]
""" reads a Horn SAT formula from a text file

:file format:
# comment
A     # clause with unique positive literal
:- A  # clause with unique negative literal
A :- B, C, D # clause where A is positive and B,C,D negative
# variables are strings without spaces
"""
formula = []
for line in open(filename, 'r'):
line = line.strip()
if line[0] == "#":
continue
lit = line.split(":-")
if len(lit) == 1:
posvar = lit[0]
negvars = []
else:
assert len(lit) == 2
posvar = lit[0].strip()
if posvar == '':
posvar = None
negvars = lit[1].split(',')
for i, _ in enumerate(negvars):
negvars[i] = negvars[i].strip()
formula.append((posvar, negvars))
return formula

# pylint: disable=line-too-long

[docs]
def horn_sat(formula):
""" Solving a HORN Sat formula

:param formula: list of couple(posvar, negvars).
negvars is a list of the negative variables (can be empty)
posvar is the positive variable (can be None)
Variables can be any hashable objects: integers, strings...
:returns: None if formula is not satisfiable, else a minimal set of vars
that have to be set to true in order to satisfy the formula.
:complexity: linear
"""
# --- construct data structures
CLAUSES = range(len(formula))
score = [0 for c in CLAUSES]  # number of neg vars not yet in solution
# the unique positive variable of a clause (if any)
posvar_in_clause = [None for c in CLAUSES]
# all clauses where a variable appears negatively
clauses_with_negvar = defaultdict(set)
for c in CLAUSES:
posvar, negvars = formula[c]
score[c] = len(set(negvars))  # do not count twice negative variables
posvar_in_clause[c] = posvar
for v in negvars:
pool = [set() for s in range(max(score) + 1)]   # create the pool
for c in CLAUSES:
pool[score[c]].add(c)           # pool[s] = set of clauses with score s

# --- 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 is None:                      # formula is not satisfiable
return None
if v in solution or curr in clauses_with_negvar[v]:
continue                       # clause is already satisfied
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

if __name__ == "__main__":