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
