22
1
Introduction
Your mission in life is simple: Prove people wrong on the internet!
To do this you usually carefully analyze their statements and point out the contradiction in them.
It's time to automate this, but as we are lazy, we want to prove people wrong with the least effort (read: shortest code) possible.
Specification
Input
Your input will be a formula in conjunctive normal form. For the format, you may use the below format or define your own, upon the needs of your language (you may not encode more in the format than the pure CNF though). The test-cases (here) are however provided in the below format (although it won't be too hard generating your own).
Your input will be a a list of a list of a list of variables (you may also read it as strings / require strings). The input is a formula in conjunctive normal form (CNF) written as a set of clauses, each being a list of two lists. The first list in the clause encodes the positive literals (variables), the second list encodes the negative (negated) literals (variables). Every variable in the clause is OR'ed together and all clauses are AND'ed together.
To make it clearer: [[[A,B],[C]],[[C,A],[B]],[[B],[A]]]
can be read as:
(A OR B OR (NOT C)) AND (C OR A OR (NOT B)) AND (B OR (NOT A))
Output
The output is boolean, e.g. either some truthy value or some falsy value.
What to do?
It's simple: Check if the formula given at hand is satisfiable, e.g. whether there exists some assignment of true and false to all variables such that the overall formula yields "true". Your output will be "true" if the formula is satiesfiable and "false" if it is not.
Fun-Fact: This is a NP-complete problem in the general case.
Note: Generating a truth-table and checking if any resulting entry is true, is allowed.
Corner Cases
If you get an empty 3rd-level list, then there's no such (positive / negative) variable in that clause - a valid input.
You can leave other corner cases undefined if you want to.
You may also return true upon an empty formula (1st level list) and false upon an empty clause (2nd level list).
Who wins?
This is code-golf so the shortest answer in bytes wins!
Standard rules apply of course.
Test-cases
[[[P],[Q,R]],[[Q,R],[P]],[[Q],[P,R]]] -> true
[[[],[P]],[[S],[]],[[R],[P]],[[U],[Q]],[[X],[R]],[[Q],[S]],[[],[P,U]],[[W],[Q,U]]] -> true
[[[],[P,Q]],[[Q,P],[]],[[P],[Q]],[[Q],[P]]] -> false
[[[P],[]],[[],[P,S]],[[P,T],[]],[[Q],[R]],[[],[R,S]],[[],[P,Q,R]],[[],[P]]] -> false
optional behavior (not mandatory, may be left undefined):
[] -> true (empty formula)
[[]] -> false (empty clause)
[[[],[]]] -> false (empty clause)
1May we take input as
(A OR B OR (NOT C)) AND (C OR A OR (NOT B)) AND (B OR (NOT A))
? – Adám – 2016-06-30T13:17:02.3901@Adám, as specified in the challenge, the format is entirely up to you, as long as it doesn't encode more information than the list-based one. (E.g. the formulation as you gave it is fully allowed) – SEJPM – 2016-06-30T13:20:19.797
@SEJPM If I understand the notation correctly, I think the 3rd and 4th test cases should return true. I tried substituting (P,Q)=(1,1) and (P,Q,R,S,T)=(0,0,0,0,0) and found both true, so there should at least be one case where the the expression is true. – busukxuan – 2016-06-30T19:29:39.290
@busukxuan, I'm 100% sure the third and fourth one are false. For the 3): this is
{{P,Q},{P,!Q},{!P,Q},{!P,!Q}}
(not in this order) which can be easily shown is a contradiction. For the 4): This is trivially a contradiction because it isP AND ... AND (NOT P)
which can obviously never be true for any value of P. – SEJPM – 2016-06-30T20:57:41.667@SEJPM Is it correct that any two non-top-level (and) expressions separated by a comma forms an or expression, so [ [], [P,Q] ] = [1,[P,Q]]=1? Also, in case 4, I see the first and final terms merely have the order inside them reversed, and to my understanding these operations are symmetric, so I don't get how one is P and the other is !P. – busukxuan – 2016-06-30T21:09:05.850
@busukxuan the outer-most list is a big AND-conjunction. The next-inner layer is a big OR-disjunktion and the two lists inside this are the positive (non-negated) and the negative (negated) variables. So
[[[],[P]]]=!P
and everything is commutative except for the two innermost lists, of which the order is used to convey the state of the literals. – SEJPM – 2016-06-30T21:21:28.1532Funny how shorter code actually requires more effort to be written. – user6245072 – 2016-07-01T07:49:01.980