# Fixing a logic system

You are given a set of logic statements. Your challenge is to remove any ones that contradict the others, but in the optimal way (i.e. removing a minimal number of statements).

### Challenge

You will write a program or a function that takes as input a list of statements, removes the minimal number of statements such that there is a solution and outputs the rest.

### Logic

Statements consist of variables A-Z and operators between them.

There are 5 operators: - (not), v (or), ^ (and), -> (if) and <-> (iff).

Truth table:

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


These operators can be combined together with parenthesis ():

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


Logic systems consist of 1 or more statements.

A solution to the logic system is a state where all of the statements are simultaneously true.

### Examples of logic systems:

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


The only solution is A = 1, B = 0.

A^B
-(B<->A)


This one has no solution; with no combination of A and B both of the statements are true.

### Input

You will receive a set of statements as input. This can be taken via STDIN or function arguments, formatted as an array (in a convenient format) or a newline-separated or space-separated string.

The statements will be of the following form (in almost-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" / "^" / "->" / "<->"


Example statements:

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


### Output

You must return the (possibly) reduced set of statements, in the exact form you received them. Again, the list can be formatted as an array of strings or a newline-separated or space-separated string.

### Rules

• You should always remove the minimal number of statements. If there are multiple possible solutions, output one of them.
• You may assume that the input always contains at least 1 statement and that no statements are repeated in the input.
• You may not assume that the output always contains a statement. (see examples)
• Using standard loopholes contradicts with your answer being valid, and one of them must be removed.
• This is , so the shortest answer in bytes wins.

### Examples

Input:

A^(-A)


Output:

(nothing)


Input:

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


Output:

A^B A<->B


Input:

["AvB","A^B"]


Output:

["AvB","A^B"]

• I don't know if this is relevant, but this problem comes down to maximum set packing, which is NP-complete. Aug 20, 2015 at 13:35
• According to your grammar, the third statement in the example is not correct ((AvB)->-B should be (AvB)->(-B)) Aug 20, 2015 at 14:15
• @proudhaskeller Thanks, corrected that. Aug 20, 2015 at 16:10
• also, parentheses in A<->(Q^C))v((-B)vH are mish-mashed. Aug 20, 2015 at 22:56
• @proudhaskeller Thanks again. Aug 20, 2015 at 23:00

# Python 3, 431 bytes

Not very golfed right now, but I figure I'd get the ball rolling with an answer. Try it here, g() is the main function.

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)

• Very cool. I got it down to 428: repl.it/BCzp Aug 21, 2015 at 14:56
• There is a problem with the way you are modeling truth values. For example, g("A (AvA)<->A") should give back its input, but it doesn't work because if A=1, then AvA=2. Aug 31, 2015 at 19:15
• Aha, you're right, thanks for pointing that out. Reverted it back to " and " for now since I couldn't think of a shorter way to compare them. Also thanks for the golfing changes Pietu! Aug 31, 2015 at 20:15
• I believe v is or. Sep 1, 2015 at 6:47
• ...yes. Thanks. Sep 1, 2015 at 12:53

# Ruby, 299298283 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

• Expects an array of expressions.
• If you're going to run it, set \$VERBOSE=nil from inside ruby so you don't get lots of warnings about redefining constants.
• Note that it actually sets the variable "v" as well but it doesn't make a difference.
• Uses truth values because they have all of the required operators already, except implication. Unfortunately Ruby doesn't have a boolean class so we have to monkey-patch Object to get implication :)
• Could make it shorter if we just set ALL of the uppercase variables, but then it would take a huge amount of time to run. Should probably have a caveat in the question about that.

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,i)})}
}
exs
else
exs.combination(exs.size-1).map{|sm|sat?(sm)}.max_by(&:size)
end
end