Introdução

Sua missão na vida é simples: prove que as pessoas estão erradas na internet!
Para fazer isso, você costuma analisar cuidadosamente as declarações deles e apontar a contradição nelas.
Está na hora de automatizar isso, mas, como somos preguiçosos, queremos provar que as pessoas estão erradas com o mínimo de esforço (leia-se: código mais curto) possível.

Especificação

Entrada

Sua entrada será uma fórmula na forma normal conjuntiva . Para o formato, você pode usar o formato abaixo ou definir o seu próprio, de acordo com as necessidades do seu idioma (você não pode codificar mais no formato do que o CNF puro). Os casos de teste (aqui) são fornecidos no formato abaixo (embora não seja muito difícil gerar o seu próprio).

Sua entrada será uma lista de uma lista de uma lista de variáveis (você também pode lê-la como strings / exigir strings). A entrada é uma fórmula na forma conjuntiva normal (CNF) escrita como um conjunto de cláusulas, cada uma sendo uma lista de duas listas. A primeira lista na cláusula codifica os literais positivos (variáveis), a segunda lista codifica os literais negativos (negados) (variáveis). Cada variável na cláusula é OR'ed juntos e todas as cláusulas são AND'ed juntos.

Para tornar mais claro: [[[A,B],[C]],[[C,A],[B]],[[B],[A]]]pode ser lido como:
(A OR B OR (NOT C)) AND (C OR A OR (NOT B)) AND (B OR (NOT A))

Saída

A saída é booleana, por exemplo, algum valor verdadeiro ou falso.

O que fazer?

É simples: verifique se a fórmula fornecida é satisfatória, por exemplo, se existe alguma atribuição de true e false para todas as variáveis, de forma que a fórmula geral produz "true". Sua saída será "true" se a fórmula for confiável e "false" se não for.
Curiosidade: Este é um problema completo de NP no caso geral.
Nota: É permitido gerar uma tabela verdade e verificar se alguma entrada resultante é verdadeira.

Estojos de canto

Se você receber uma lista de terceiro nível vazia, não haverá essa variável (positiva / negativa) nessa cláusula - uma entrada válida.
Você pode deixar outros casos de canto indefinidos, se desejar.
Você também pode retornar verdadeiro em uma fórmula vazia (lista do 1º nível) e falso em uma cláusula vazia (lista do 2º nível).

Quem ganha?

Isso é código-golfe, então a resposta mais curta em bytes vence!
Regras padrão se aplicam, é claro.

Casos de teste

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

Mathematica, 12 bytes

SatisfiableQ

Bem, há um built-in ...

O formato de entrada é And[Or[a, b, Not[c], Not[d]], Or[...], ...]. Isso faz o trabalho corretamente para sub-expressões vazias, porque Or[]é Falsee And[]é True.

Para o registro, uma solução que recebe o formato baseado em lista do desafio e realiza a conversão em si é de 44 bytes, mas o OP esclareceu em um comentário que qualquer formato é bom desde que não codifique nenhuma informação adicional:

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

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)

Esse desafio merece uma resposta sem construção, então aqui está. Experimente em ideone . O algoritmo simplesmente tenta todas as atribuições de variáveis ​​e verifica se uma delas satisfaz a fórmula.

A entrada está na forma de [([],["P","Q"]),(["Q","P"],[]),(["P"],["Q"]),(["Q"],["P"])], embora, em vez de cadeias, todo tipo com igualdade funcione.

Código não destruído:

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)

Uso:

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