Блог

Программа на Python, которая, учитывая формулу SAT в форме 3-CNF, определяет, является ли формула выполнимой, и если да, то выводит удовлетворительное назначение истинности.

То, что у меня сейчас есть:

 def brute_force(cnf):  literals = set()  for conj in cnf:  for disj in conj:  literals.add(disj[0])    literals = list(literals)  n = len(literals)  for seq in itertools.product([True,False], repeat=n):  a = set(zip(literals, seq))  if all([bool(disj.intersection(a)) for disj in cnf]):  return True, a    return False, None