Вам дан набор логических утверждений. Ваша задача состоит в том, чтобы удалить любые из них, которые противоречат другим, но оптимальным образом (т.е. удалить минимальное количество утверждений).

Вызов

Вы напишите программу или функцию, которая принимает в качестве входных данных список операторов, удаляет минимальное количество операторов, так что есть решение, и выводит остальные.

логика

Утверждения состоят из переменных A-Z и операторов между ними.

Есть 5 операторов : -(не), v(или), ^(и), ->(если) и <->(если).

Таблица правды:

A | B | -A | AvB | A^B | A->B | A<->B
0 | 0 |  1 |  0  |  0  |   1  |   1
0 | 1 |  1 |  1  |  0  |   1  |   0
1 | 0 |  0 |  1  |  0  |   0  |   0
1 | 1 |  0 |  1  |  1  |   1  |   1

Эти операторы могут быть объединены вместе с круглыми скобками ():

A | B | -(AvB) | Av(-A) | A^(-A) | (AvB)->(-B)
0 | 0 |    1   |    1   |    0   |      1
0 | 1 |    0   |    1   |    0   |      0
1 | 0 |    0   |    1   |    0   |      1
1 | 1 |    0   |    1   |    0   |      0

Логические системы состоят из 1 или более операторов .

Решение для логической системы является состояние , в котором все заявления одновременно являются правдой.

Примеры логических систем:

AvB
-(A<->B)
(AvB)->(-B)

Единственное решение есть A = 1, B = 0.

A^B
-(B<->A)

У этого нет решения ; без комбинации Aи Bоба утверждения верны.

вход

Вы получите набор утверждений в качестве входных данных. Это может быть принято через STDIN или аргументы функции, отформатированные в виде массива (в удобном формате) или строки, разделенной символом новой строки или пробелом.

Заявления будут иметь следующую форму (в почти ABNF ):

statement        = variable / operation
operation        = not-operation / binary-operation
not-operation    = "-" operand
binary-operation = operand binary-operator operand
operand          = variable / "(" operation ")"
variable         = "A"-"Z"
binary-operator  = "v" / "^" / "->" / "<->"

Пример заявления:

A
Av(-B)
(A<->(Q^C))v((-B)vH)

Выход

Вы должны возвратить (возможно) сокращенный набор утверждений в том виде, в каком вы их получили. Опять же, список может быть отформатирован как массив строк или строки, разделенные символом новой строки или пробелом.

правила

• Вы должны всегда удалять минимальное количество утверждений. Если существует несколько возможных решений, выведите одно из них.
• Вы можете предположить, что входные данные всегда содержат хотя бы 1 оператор и что никакие операторы не повторяются во входных данных.
• Вы не можете предполагать, что выходные данные всегда содержат оператор. (см. примеры)
• Использование стандартных лазеек противоречит тому, что ваш ответ является действительным, и одна из них должна быть удалена.
• Это код-гольф , поэтому выигрывает самый короткий ответ в байтах.

Примеры

Входные данные:

A^(-A)

Выход:

(nothing)

Входные данные:

A^B A<->(-B) A<->B

Выход:

A^B A<->B

Входные данные:

["AvB","A^B"]

Выход:

["AvB","A^B"]

Рубин, 299 298 283 279 байт

class Object;def * o;!self|o;end;def s;w=join.gsub(/\W/,"").chars.uniq;n=w.size;(0..2**n).any?{|i|n.times{|j|eval(w[j]+"=#{i[j]>0}")};all?{|e|eval([%w[<-> ==],%w[-> *],%w[- !],%w[^ &],%w[v |]].inject(e){|x,i|x.gsub(*i)})}}?self:combination(size-1).map(&:s).max_by(&:size);end;end

• Ожидается массив выражений.
• Если вы собираетесь его запустить, установите $ VERBOSE = nil внутри ruby, чтобы вы не получали много предупреждений о переопределении констант.
• Обратите внимание, что он также устанавливает переменную "v", но это не имеет значения.
• Использует значения истинности, потому что у них уже есть все необходимые операторы, кроме импликации. К сожалению, в Ruby нет логического класса, поэтому мы должны сделать патч для объекта, чтобы получить смысл :)
• Можно было бы сделать его короче, если бы мы просто установили ВСЕ переменные в верхнем регистре, но тогда для запуска потребовалось бы огромное количество времени. Вероятно, следует иметь оговорку в вопросе об этом.

Ungolfed:

class Object
  def * o 
    !self|o
  end 
end

def sat? exs 
  #exs: an array of expressions
  s=[%w[<-> ==], %w[-> *], "-!", "^&", %w[v ||]]

  w=exs.join.gsub(/\W/,"").chars.uniq #variable names
  n=w.size
  if (0...2**n).any? {|i|
    n.times do |vi|
      eval("#{w[vi]}=#{i[vi]==1}")
    end 
    exs.all?{|ex|eval(s.inject(ex){|x,i|x.gsub(i[0],i[1])})}
  }
    exs
  else
    exs.combination(exs.size-1).map{|sm|sat?(sm)}.max_by(&:size)
  end
end

Python 3, 431 байт

Сейчас я не очень играю в гольф, но думаю, что получу ответ. Попробуйте здесь , g()это основная функция.

import re,itertools as H
def g(i):
 y=re.sub(r'\W','',''.join(set(i)).upper());l=i.split()
 def e(s):
  def f(a):
   for v,w in a:exec(v+'='+w)
   return eval(re.sub('[^A-Z()]+',lambda x:{'v':' or ','^':'*','<->':'==','->':'<=','-':'not '}[x.group()],s))
  return[c for c in H.product("01",repeat=len(y))if f(zip(y,c))]
 for n in range(len(l),-1,-1):
  for q in H.combinations(l,n):
   if e('('+')^('.join(q)+')'):return' '.join(q)