# Prove me wrong!

## 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)

• May we take input as (A OR B OR (NOT C)) AND (C OR A OR (NOT B)) AND (B OR (NOT A))? – Adám Jun 30 '16 at 13:17
• @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 Jun 30 '16 at 13:20
• @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 Jun 30 '16 at 19:29
• @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 is P AND ... AND (NOT P) which can obviously never be true for any value of P. – SEJPM Jun 30 '16 at 20:57
• Funny how shorter code actually requires more effort to be written. – user6245072 Jul 1 '16 at 7:49

## Mathematica, 12 bytes

SatisfiableQ


Well, there's a built-in...

Input format is And[Or[a, b, Not[c], Not[d]], Or[...], ...]. This does work correctly for empty sub-expressions, because Or[] is False and And[] is True.

For the record, a solution which receives the list-based format from the challenge and does the conversion itself is 44 bytes, but the OP clarified in a comment that any format is fine as long as it doesn't encode any additional information:

SatisfiableQ[Or@@Join[#,Not/@#2]&@@@And@@#]&

• Because Mathematica... – Leaky Nun Jun 30 '16 at 13:24
• Mathematica really have a insane number of builtin ._. – TuxCrafting Jun 30 '16 at 13:27
• @TùxCräftîñg Indeed. – jpmc26 Jun 30 '16 at 16:20
• For split-second, I thought this answer was written in an obscure, stacked-based esolang where, by mere chance, the command sequence S a t i s f i a b l e Q would solve the problem. Only then, reading comprehension knocked on the door... – ojdo Jun 30 '16 at 21:00

t=1<3
e%((t,f):r)=or((e<\$>t)++map(not.e)f)&&e%r
e%_=t
u v b e s|s==v=b|t=e s
s e[]c=1<0
s e(v:w)c=e%c||s(u v t e)w c||s(u v(1<0)e)w c
g v[]=v
g v((t,f):r)=g(v++[x|x<-t++f,notElem x v])r
g[]>>=s(\x->t)


This challenge deserves a no-build-in answer, so here you go. Try it on ideone. The algorithm simply tries all variable assignments and checks whether one of them satisfies the formula.

Input is in the form of [([],["P","Q"]),(["Q","P"],[]),(["P"],["Q"]),(["Q"],["P"])], although instead of strings every type with equality will work.

### Ungolfed code:

type Variable   = String
type CNF        = [([Variable], [Variable])]
type Evaluation = (Variable -> Bool)

satisfies :: Evaluation -> CNF -> Bool
satisfies eval [] = True
satisfies eval ((t,f):r) = or(map eval t ++ map (not.eval) f) && satisfies eval r

update :: Evaluation -> Variable -> Bool -> Evaluation
update eval s b var = if var == s then b else eval var

search :: Evaluation -> [Variable] -> CNF -> Bool
search eval [] cnf = False
search eval (v:vars) cnf = satisfies eval cnf || search (update eval v True) vars cnf || search (update eval v False) vars cnf

getVars :: CNF -> [Variable] -> [Variable]
getVars [] vars = vars
getVars ((t,f):cnf) vars = getVars cnf (vars ++ [v |v<-(t++f), notElem v vars])

isSat :: CNF -> Bool
isSat cnf = search (\x->True) (getVars cnf []) cnf


# JavaScript 6, 69B

x=>f=(v,e)=>(e=v.pop())?[0,1].some(t=>f([...v],eval(e+'=t'))):eval(x)


Usage:

f('a|b')(['a','b'])
true