Problem hidden
|This problem was hidden by Editorial Board member probably because it has incorrect language|version or invalid test data, or description of the problem is not clear.|

AL_29_02 - SAT Solver

Mały Jaś uczęszcza na zajęcia dla wybitnie uzdolnionych matematycznie gdzie ostatnio tematem był bardzo ważny problem spełnialności formuł logicznych. W problemie tym mamy na wejściu formułę logiczną i musimy rozstrzygnąć czy istnieje wartościowanie występujących w niej zmiennych dla którego formuła ta jest prawdziwa. Okazało się, że wiele problemów algorytmicznych redukuje się do problemu spełnialności. Przykładem takiego problemu jest słynny problem istnienia cyklu Hamiltona - można go sformułować jako problem spełnialności pewnej formuły (zależnej od badanego grafu). Nie byłoby to jednak zbyt zaskakujące gdyby nie fakt, że taką formułę można skonstruować w czasie wielomianowym od rozmiaru opisu grafu.

Jaś prowadzi już własne badania. Udało mu się przedstawić pewien problem jako instancję problemu spełnialności. Otrzymana przez niego formuła jest jednak bardzo szczególnej postaci. Składa się z alternatywy klauzul. Klauzulą nazywamy koniunkcję literałów (zmienna bądź jej zaprzeczenie). Teraz potrzebuje tylko programu, który sprawdzi jego wyniki i rozstrzygnie czy otrzymana formuła jest spełnialna. Jako że jest teoretykiem poprosił Ciebie o pomoc.

Wejście

Wejście rozpoczyna liczba testów 1 <= t <= 1000. Każdy test rozpoczynają liczby 1 <= n <= 1000 oraz 1 <= k <= 100 oznaczające kolejno liczbę klauzul formuły oraz liczbę jej zmiennych. Następnie znajdują się opisy kolejnych klauzul. Opis klauzuli rozpoczyna się liczbą 1 <= d <= 100 oznaczającą liczbę literałów, po której następuje d liczb całkowitych opisujących kolejne literały w tej klauzuli. Każdy literał przedstawia różna od zera liczba z zakresu [-k; k]. Jeśli ta liczba i jest dodatnia to znaczy że w klauzuli występuje i-ta zmienna. Jeśli liczba ta jest ujemna to znaczy, że w klauzuli występuje negacja i-tej zmiennej.

Wyjście

Dla każdego testu należy wypisać "TAK" jeśli formuła logiczna jest spełnialna, "NIE" w przeciwnym przypadku.

Przykład

Wejście:
1
2 2
2 1 -2
1 -2

Wyjście: TAK

Wyjaśnienie do przykładu:

Test odpowiada formule logicznej (x1 /\ ~x2) \/ ~x2 której wartościowanie spełniające to na przykład x1 = 1, x2 = 0.

Dodane przez:Adam Bąk
Data dodania:2016-08-25
Limit czasu wykonania programu:1s
Limit długości kodu źródłowego50000B
Limit pamięci:1536MB
Cluster: Cube (Intel G860)
Języki programowania:All except: ASM64 GOSU
© Spoj.com. All Rights Reserved. Spoj uses Sphere Engine™ © by Sphere Research Labs.