Zgłaszanie | Wszystkie zgłoszenia | Najlepsze | Lista |
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łowego | 50000B |
Limit pamięci: | 1536MB |
Cluster: | Cube (Intel G860) |
Języki programowania: | All except: ASM64 GOSU |