Prove me wrong!

Question

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)

Answer 1

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@@#]&

Answer 2

Haskell, 203 200 bytes

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

Answer 3

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