Greedy algorithm for SAT — различия между версиями

Текущая версия на 10:37, 18 декабря 2017

Вход

Множество дизъюнктов С от n переменных x_j

Найти

Значения x, максимизирующие число выполненных дизъюнктов.

  for j in range(x):
      x[j] :=  True
 
  repeat
      l := литерал, который встречается в наибольшем числе скобок в C # Если несколько — пофиг какой
      С_in_which_l :=  набор дизъюнктов-скобок, где есть "l"
      C_in_which_not_l := набор дизъюнктов-скобок, где есть "not l"
      x_l := переменная для этого l;
 
      if l — литерал в положительной степени:
            C:= C - С_in_which_l
            удалить "not l" из всех дизъюнктов из C_in_which_not_l
      else:   
            x_l = False
            C:= C - С_in_which_not_l
            удалить "l" из всех дизъюнктов из C_in_which_not_l
 
      Удалить все пусктые скобки из C
  until len(C)==0;
  return x