Просмотр исходного текста страницы Greedy algorithm for SAT


;Вход: Множество дизъюнктов С от n переменных x_j
;Найти: Значения x, максимизирующие число выполненных дизъюнктов.
<code-python>
  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
</code-python>