<SYSTEM_TASK:>
Solve the following problem using Python, implementing the functions described below, one line at a time
<END_TASK>
<USER_TASK:>
Description:
 def read(filename):
 """ 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 range(len(negvars)):
                negvars[i] = negvars[i].strip()
        formula.append((posvar, negvars))
    return formula