16
\$\begingroup\$

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"]
\$\endgroup\$
  • 3
    \$\begingroup\$ I don't know if this is relevant, but this problem comes down to maximum set packing, which is NP-complete. \$\endgroup\$ – Leif Willerts Aug 20 '15 at 13:35
  • \$\begingroup\$ According to your grammar, the third statement in the example is not correct ((AvB)->-B should be (AvB)->(-B)) \$\endgroup\$ – proud haskeller Aug 20 '15 at 14:15
  • \$\begingroup\$ @proudhaskeller Thanks, corrected that. \$\endgroup\$ – PurkkaKoodari Aug 20 '15 at 16:10
  • \$\begingroup\$ also, parentheses in A<->(Q^C))v((-B)vH are mish-mashed. \$\endgroup\$ – proud haskeller Aug 20 '15 at 22:56
  • \$\begingroup\$ @proudhaskeller Thanks again. \$\endgroup\$ – PurkkaKoodari Aug 20 '15 at 23:00
3
+100
\$\begingroup\$

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
  • 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[0],i[1])})}
  }
    exs
  else
    exs.combination(exs.size-1).map{|sm|sat?(sm)}.max_by(&:size)
  end
end
\$\endgroup\$
5
\$\begingroup\$

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)
\$\endgroup\$
  • \$\begingroup\$ Very cool. I got it down to 428: repl.it/BCzp \$\endgroup\$ – PurkkaKoodari Aug 21 '15 at 14:56
  • \$\begingroup\$ 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. \$\endgroup\$ – Ibrahim Tencer Aug 31 '15 at 19:15
  • \$\begingroup\$ 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! \$\endgroup\$ – TheMadHaberdasher Aug 31 '15 at 20:15
  • \$\begingroup\$ I believe v is or. \$\endgroup\$ – PurkkaKoodari Sep 1 '15 at 6:47
  • \$\begingroup\$ ...yes. Thanks. \$\endgroup\$ – TheMadHaberdasher Sep 1 '15 at 12:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.