Wprowadzenie

Twoja misja w życiu jest prosta: Udowodnij ludziom, że się mylą w Internecie!
W tym celu zazwyczaj dokładnie analizuje się ich wypowiedzi i wskazuje na zawarte w nich sprzeczności.
Czas to zautomatyzować, ale ponieważ jesteśmy leniwi, chcemy udowodnić, że ludzie się mylą przy jak najmniejszym wysiłku (czytaj: najkrótszy kod).

Specyfikacja

Wkład

Twój wkład będzie formułą w spójnej normalnej formie . W tym formacie możesz użyć poniższego formatu lub zdefiniować własny, zgodnie z potrzebami swojego języka (nie możesz jednak kodować więcej w formacie niż czysty CNF). Przypadki testowe (tutaj) są jednak dostarczone w poniższym formacie (chociaż wygenerowanie własnego nie będzie trudne).

Twoje dane wejściowe będą listą listy zmiennych (możesz także odczytać ją jako ciągi / wymagają ciągów). Dane wejściowe to formuła w spójnej postaci normalnej (CNF) napisana jako zestaw klauzul, z których każda jest listą dwóch list. Pierwsza lista w klauzuli koduje literały dodatnie (zmienne), druga lista koduje literały ujemne (negowane) (zmienne). Każda zmienna w klauzuli jest OR'ed razem, a wszystkie klauzule AND'ed razem.

Aby było jaśniej: [[[A,B],[C]],[[C,A],[B]],[[B],[A]]]można odczytać jako:
(A OR B OR (NOT C)) AND (C OR A OR (NOT B)) AND (B OR (NOT A))

Wydajność

Wyjście ma wartość logiczną, np. Albo pewna wartość prawdy, albo pewna wartość fałszu.

Co robić?

To proste: Sprawdź, czy podana formuła jest zadowalająca, np. Czy istnieje przypisanie wszystkich zmiennych prawda i fałsz, tak aby ogólna formuła dawała „prawda”. Twoje wyniki będą „prawdziwe”, jeśli formuła będzie satysfakcjonująca, i „fałszywe”, jeśli nie będzie.
Ciekawostka: w ogólnym przypadku jest to problem NP-zupełny.
Uwaga: Dozwolone jest generowanie tabeli prawdy i sprawdzanie, czy jakikolwiek wynikowy wpis jest prawdziwy.

Obudowy narożne

Jeśli otrzymasz pustą listę trzeciego poziomu, nie ma takiej zmiennej (dodatniej / ujemnej) w tej klauzuli - prawidłowe dane wejściowe.
Jeśli chcesz, możesz pozostawić nieokreślone inne skrzynki narożne.
Możesz także zwrócić wartość true przy pustej formule (lista 1. poziomu) i false przy pustej klauzuli (lista 2. poziomu).

Kto wygrywa?

To jest golf golfowy, więc wygrywa najkrótsza odpowiedź w bajtach!
Oczywiście obowiązują standardowe zasady.

Przypadki testowe

[[[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 bajtów

SatisfiableQ

Cóż, jest wbudowany ...

Format wejściowy to And[Or[a, b, Not[c], Not[d]], Or[...], ...]. Działa to poprawnie dla pustych podwyrażeń, ponieważ Or[]jest Falsei And[]jest True.

Dla przypomnienia, rozwiązanie, które odbiera format oparty na liście od wyzwania i dokonuje samej konwersji, ma 44 bajty, ale OP wyjaśnił w komentarzu, że dowolny format jest w porządku, o ile nie koduje żadnych dodatkowych informacji:

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

Haskell, 203 200 bajtów

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)

To wyzwanie zasługuje na odpowiedź niewbudowaną, więc proszę bardzo. Wypróbuj na ideone . Algorytm po prostu próbuje wszystkich przypisań zmiennych i sprawdza, czy jedno z nich spełnia formułę.

Dane wejściowe mają postać [([],["P","Q"]),(["Q","P"],[]),(["P"],["Q"]),(["Q"],["P"])], chociaż zamiast łańcuchów każdy typ z równością będzie działał.

Nieskluczony kod:

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)

Stosowanie:

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