introduction

Votre mission dans la vie est simple: prouver que les gens ont tort sur Internet!
Pour ce faire, vous analysez généralement attentivement leurs déclarations et signalez leur contradiction.
Il est temps d'automatiser cela, mais comme nous sommes paresseux, nous voulons prouver que les gens ont tort avec le moins d'effort possible (lire: code le plus court) possible.

spécification

Contribution

Votre entrée sera une formule sous forme normale conjonctive . Pour le format, vous pouvez utiliser le format ci-dessous ou définir le vôtre, selon les besoins de votre langue (vous ne pouvez cependant pas encoder plus dans le format que le CNF pur). Les cas de test (ici) sont cependant fournis dans le format ci-dessous (bien qu'il ne soit pas trop difficile de générer le vôtre).

Votre entrée sera une liste d'une liste d'une liste de variables (vous pouvez également la lire sous forme de chaînes / exiger des chaînes). L'entrée est une formule sous forme normale conjonctive (CNF) écrite comme un ensemble de clauses, chacune étant une liste de deux listes. La première liste de la clause code les littéraux positifs (variables), la seconde liste code les littéraux négatifs (négatifs) (variables). Chaque variable de la clause est OU ensemble et toutes les clauses sont ET ensemble.

Pour être plus clair: [[[A,B],[C]],[[C,A],[B]],[[B],[A]]]peut être lu comme:
(A OR B OR (NOT C)) AND (C OR A OR (NOT B)) AND (B OR (NOT A))

Sortie

La sortie est booléenne, par exemple, soit une valeur vraie ou une valeur fausse.

Que faire?

C'est simple: vérifiez si la formule donnée à la main est satisfaisable, par exemple s'il existe une affectation de vrai et de faux à toutes les variables de sorte que la formule globale donne "vrai". Votre résultat sera "vrai" si la formule est satisfaisante et "faux" dans le cas contraire.
Fun-Fact: Il s'agit d'un problème NP-complet dans le cas général.
Remarque: La génération d'une table de vérité et la vérification de la véracité d'une entrée résultante sont autorisées.

Étuis d'angle

Si vous obtenez une liste de 3e niveau vide, il n'y a pas de variable (positive / négative) dans cette clause - une entrée valide.
Vous pouvez laisser d'autres cas d'angle indéfinis si vous le souhaitez.
Vous pouvez également retourner true sur une formule vide (liste de 1er niveau) et false sur une clause vide (liste de 2e niveau).

Qui gagne?

Il s'agit de code-golf, donc la réponse la plus courte en octets l'emporte!
Les règles standard s'appliquent bien sûr.

Cas de test

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

SatisfiableQ

Eh bien, il y a un intégré ...

Le format d'entrée est And[Or[a, b, Not[c], Not[d]], Or[...], ...]. Cela fait correctement le travail pour les sous-expressions vides, parce Or[]est Falseet And[]est True.

Pour mémoire, une solution qui reçoit le format basé sur une liste du défi et effectue la conversion elle-même est de 44 octets, mais l'OP a précisé dans un commentaire que tout format est correct tant qu'il ne code pas d'informations supplémentaires:

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

Haskell, 203 200 octets

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)

Ce défi mérite une réponse non intégrée, alors voilà. Essayez-le sur ideone . L'algorithme essaie simplement toutes les affectations de variables et vérifie si l'une d'entre elles satisfait la formule.

L'entrée est sous la forme de [([],["P","Q"]),(["Q","P"],[]),(["P"],["Q"]),(["Q"],["P"])], bien qu'au lieu de chaînes, chaque type avec égalité fonctionnera.

Code non golfé:

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