Te dan un conjunto de declaraciones lógicas. Su desafío es eliminar los que contradicen a los demás, pero de la manera óptima (es decir, eliminar un número mínimo de declaraciones).

Desafío

Escribirás un programa o una función que tome como entrada una lista de declaraciones, elimine el número mínimo de declaraciones de modo que haya una solución y genere el resto.

Lógica

Las declaraciones consisten en variables A-Z y operadores entre ellas.

Hay 5 operadores : -(no), v(o), ^(y), ->(if) y <->(iff).

Mesa de la verdad:

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

Estos operadores se pueden combinar junto con paréntesis ():

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

Los sistemas lógicos consisten en 1 o más declaraciones .

Una solución para el sistema lógico es un estado en el que todas las declaraciones son simultáneamente verdaderas.

Ejemplos de sistemas lógicos:

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

La única solución es A = 1, B = 0.

A^B
-(B<->A)

Este no tiene solución ; sin combinación de Ay Bambas afirmaciones son verdaderas.

Entrada

Recibirá un conjunto de declaraciones como entrada. Esto se puede tomar a través de STDIN o argumentos de función, formateados como una matriz (en un formato conveniente) o una cadena separada por líneas o espacios separados.

Las declaraciones serán de la siguiente forma (en casi 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" / "^" / "->" / "<->"

Declaraciones de ejemplo:

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

Salida

Debe devolver el (posiblemente) conjunto reducido de declaraciones, en la forma exacta en que las recibió. Una vez más, la lista se puede formatear como una matriz de cadenas o una cadena separada por líneas o espacios separados.

Reglas

• Siempre debe eliminar el número mínimo de declaraciones. Si hay varias soluciones posibles, envíe una de ellas.
• Puede suponer que la entrada siempre contiene al menos 1 instrucción y que ninguna instrucción se repite en la entrada.
• No puede suponer que la salida siempre contiene una declaración. (ver ejemplos)
• El uso de lagunas estándar contradice que su respuesta sea válida, y una de ellas debe eliminarse.
• Este es el código de golf , por lo que gana la respuesta más corta en bytes.

Ejemplos

Entrada:

A^(-A)

Salida:

(nothing)

Entrada:

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

Salida:

A^B A<->B

Entrada:

["AvB","A^B"]

Salida:

["AvB","A^B"]

Rubí, 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

• Espera una serie de expresiones.
• Si va a ejecutarlo, establezca $ VERBOSE = nil desde dentro de ruby ​​para que no reciba muchas advertencias sobre la redefinición de constantes.
• Tenga en cuenta que en realidad también establece la variable "v", pero no hace la diferencia.
• Utiliza valores de verdad porque ya tienen todos los operadores requeridos, excepto la implicación. Desafortunadamente, Ruby no tiene una clase booleana, por lo que tenemos que hacer un parche en el objeto para obtener implicación :)
• Podría hacerlo más corto si solo configuramos TODAS las variables en mayúsculas, pero luego tomaría una gran cantidad de tiempo ejecutarlo. Probablemente debería tener una advertencia en la pregunta sobre eso.

Sin golf:

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

No estoy muy golfizado en este momento, pero me imagino que pondría la pelota en marcha con una respuesta. Pruébalo aquí , g()es la función principal.

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)