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,
[docs]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 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: clauses_with_negvar[v].add(c) 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 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
if __name__ == "__main__": F = read(sys.argv[1]) sol = horn_sat(F) if sol is None: print("No solution") else: print("Minimal solution:") for x in sorted(sol): print(x)