Sie erhalten eine Reihe von logischen Anweisungen. Ihre Herausforderung besteht darin, diejenigen zu entfernen, die im Widerspruch zu den anderen stehen, jedoch auf optimale Weise (dh, eine minimale Anzahl von Anweisungen zu entfernen).

Herausforderung

Sie schreiben ein Programm oder eine Funktion, die eine Liste von Anweisungen als Eingabe verwendet, die minimale Anzahl von Anweisungen entfernt, sodass es eine Lösung gibt, und den Rest ausgibt.

Logik

Anweisungen bestehen aus Variablen A-Z und Operatoren zwischen ihnen.

Es gibt 5 Operatoren : -(nicht), v(oder), ^(und), ->(wenn) und <->(wennf).

Wahrheitstabelle:

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

Diese Operatoren können mit Klammern kombiniert werden ():

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

Logiksysteme bestehen aus einer oder mehreren Anweisungen .

Eine Lösung für das Logiksystem ist ein Zustand, in dem alle Aussagen gleichzeitig wahr sind.

Beispiele für Logiksysteme:

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

Die einzige Lösung ist A = 1, B = 0.

A^B
-(B<->A)

Dieser hat keine Lösung ; Ohne Kombination von Aund sind Bbeide Aussagen wahr.

Eingang

Sie erhalten eine Reihe von Anweisungen als Eingabe. Dies kann über STDIN oder Funktionsargumente erfolgen, die als Array (in einem geeigneten Format) oder als durch Zeilenumbrüche oder Leerzeichen getrennte Zeichenfolge formatiert sind.

Die Aussagen haben die folgende Form (fast in 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" / "^" / "->" / "<->"

Beispielanweisungen:

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

Ausgabe

Sie müssen die (möglicherweise) reduzierten Aussagen in der genauen Form zurücksenden, in der Sie sie erhalten haben. Auch hier kann die Liste als Array von Zeichenfolgen oder als durch Zeilenumbrüche oder Leerzeichen getrennte Zeichenfolge formatiert werden.

Regeln

• Sie sollten immer die minimale Anzahl von Anweisungen entfernen. Wenn es mehrere mögliche Lösungen gibt, geben Sie eine davon aus.
• Sie können davon ausgehen, dass die Eingabe immer mindestens 1 Anweisung enthält und dass in der Eingabe keine Anweisungen wiederholt werden.
• Sie können nicht davon ausgehen, dass die Ausgabe immer eine Anweisung enthält. (siehe Beispiele)
• Die Verwendung von Standardlücken widerspricht der Gültigkeit Ihrer Antwort und eine davon muss entfernt werden.
• Das ist Code-Golf , also gewinnt die kürzeste Antwort in Bytes.

Beispiele

Eingang:

A^(-A)

Ausgabe:

(nothing)

Eingang:

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

Ausgabe:

A^B A<->B

Eingang:

["AvB","A^B"]

Ausgabe:

["AvB","A^B"]

Ruby, 299 298 283 279 Bytes

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

• Erwartet eine Reihe von Ausdrücken.
• Wenn Sie es ausführen möchten, setzen Sie $ VERBOSE = nil in ruby, damit Sie nicht viele Warnungen erhalten, wenn Sie Konstanten neu definieren.
• Beachten Sie, dass es tatsächlich auch die Variable "v" setzt, aber keinen Unterschied macht.
• Verwendet Wahrheitswerte, da sie mit Ausnahme der Implikation bereits alle erforderlichen Operatoren haben. Leider hat Ruby keine Boolesche Klasse, daher müssen wir das Affen-Patch-Objekt ausführen, um Implikationen zu erhalten :)
• Könnte es kürzer machen, wenn wir nur ALLE Großbuchstaben setzen, aber dann würde es sehr viel Zeit in Anspruch nehmen, um ausgeführt zu werden. Sollte wahrscheinlich eine Einschränkung in der Frage dazu haben.

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 Bytes

Im Moment nicht sehr golfen, aber ich denke, ich würde den Ball mit einer Antwort ins Rollen bringen. Probieren Sie es hier , g()ist die Hauptfunktion.

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)