Każda zagadka Griductive składa odważną obietnicę: nigdy nie będziesz musiał zgadywać. Każdą komórkę można ustalić wyłącznie za pomocą logiki, a każda zagadka ma dokładnie jedną poprawną odpowiedź.
To nie jest cel projektowy — to matematyczna gwarancja, wymuszana przez tę samą klasę solverów, która jest używana w badaniach operacyjnych i weryfikacji układów scalonych. Ten wpis wyjaśnia, jak to działa.
Dlaczego unikalność ma znaczenie
Jeśli zagadka ma dwa poprawne rozwiązania, musi istnieć co najmniej jedna komórka, w której zarówno Podejrzany, jak i Niewinny spełniają wszystkie wskazówki. W takiej komórce żadne rozumowanie nie powie ci, która odpowiedź jest prawidłowa — musiałbyś zgadywać. Zgadywanie łamie podstawową zasadę zagadki dedukcyjnej.
Dlatego generator nie tworzy po prostu zagadek, które akurat mają jedno rozwiązanie. On udowadnia, że drugie rozwiązanie nie istnieje, zanim zagadka zostanie kiedykolwiek opublikowana.
Pięciofazowy potok
Każda zagadka Griductive jest budowana w pięciofazowym potoku. Oto, co dzieje się na każdym etapie.
Faza 1: Generowanie losowego rozwiązania
Generator zaczyna od utworzenia prawidłowej siatki rozwiązania — losowego przypisania Podejrzanego lub Niewinnego do każdej komórki. To jest stan bazowy, który gracz ostatecznie wydedukuje.
Na tym etapie nie istnieją jeszcze żadne wskazówki. Plansza to po prostu losowa konfiguracja spełniająca podstawowe ograniczenia strukturalne (wymiary siatki, liczba podejrzanych w dopuszczalnych zakresach).
Faza 2: Budowanie puli wskazówek
Następnie generator wyczerpująco wylicza każdą możliwą wskazówkę, która jest prawdziwa na planszy rozwiązania.
Griductive ma ponad 26 różnych typów wskazówek — zliczające, porównawcze, przestrzenne, egzystencjalne, unikalności, łączności i inne. Dla każdego typu generator testuje każdą prawidłową parametryzację na planszy. Siatka 4×4 może wygenerować tysiące kandydatów na wskazówki. Zachowywane są tylko wskazówki, które ewaluują się jako true (prawda) na rozwiązaniu.
To jest surowiec, z którym pracuje generator: ogromna pula prawdziwych stwierdzeń, z których większość jest redundantna.
Faza 3: Wybór minimalnego zestawu wskazówek (najtrudniejsza część)
To jest etap, na którym odbywa się prawdziwa praca. Generator musi wybrać mały podzbiór wskazówek z puli, tak aby:
- Wskazówki były wystarczające — razem ograniczały przestrzeń rozwiązań do dokładnie jednej prawidłowej planszy.
- Żadna wskazówka nie była zbędna — usunięcie dowolnej pojedynczej wskazówki pozwalałoby na wiele rozwiązań.
Generator stosuje podejście zachłannego spełniania ograniczeń:
- Zacznij bez wybranych wskazówek. Przestrzeń rozwiązań jest szeroko otwarta — wiele plansz mogłoby być prawidłowych.
- Oceń każdą kandydującą wskazówkę pod kątem tego, jak bardzo zawęża przestrzeń rozwiązań. Wskazówka eliminująca 80% pozostałych możliwości otrzymuje wyższy wynik niż ta eliminująca 10%.
- Wybierz wskazówkę z najwyższym wynikiem i dodaj ją do zestawu.
- Ponownie rozwiąż model ograniczeń ze zaktualizowanym zestawem wskazówek.
- Powtarzaj, aż solver potwierdzi, że pozostało tylko jedno rozwiązanie.
- Przycinanie: przejdź przez końcowy zestaw i usuń wskazówki, które nie są konieczne do zachowania unikalności. Dzięki temu zagadka jest czysta i gracz nie dostaje darmowych informacji.
Rezultatem jest zwarty, uczciwy zestaw wskazówek — wystarczający do pełnego rozwiązania zagadki, bez zbędnych elementów.
Faza 4: Ocena trudności
Po ustaleniu zestawu wskazówek generator ocenia trudność zagadki w skali 0–100. Cztery czynniki mają wpływ:
- Proporcja prostych wskazówek (35%) — Ile wskazówek to bezpośrednie zliczenia lub stwierdzenia tożsamości. Więcej prostych wskazówek oznacza łatwiejszą zagadkę.
- Proporcja złożonych wskazówek (30%) — Ile wskazówek wymaga wieloetapowego lub przestrzennego rozumowania. Te wymagają głębszych łańcuchów dedukcji.
- Niedobór informacji (20%) — Jak mało wskazówek podano w stosunku do rozmiaru siatki. Mniej wskazówek oznacza mniej materiału do pracy.
- Skala siatki (15%) — Większe siatki są z natury trudniejsze do śledzenia. Zagadka 5×5 ma prawie trzy razy więcej komórek niż 3×3.
Każdy typ wskazówki ma również wewnętrzną ocenę złożoności opartą na wymaganym rozumowaniu. Wskazówka typu „Julia jest podejrzaną" jest niemal najprostsza, jak to możliwe. Wskazówka typu „Julia jest jedyną osobą w wierszu 3, która ma dokładnie 1 podejrzanego sąsiada" wymaga sprawdzenia wielu komórek i otrzymuje znacznie wyższą ocenę.
Faza 5: Generowanie podpowiedzi i formatowanie wyjścia
Na koniec generator buduje sekwencję podpowiedzi — zalecaną kolejność rozwiązywania, która prowadzi zagubionych graczy przez zagadkę, jeden logiczny krok na raz. Podpowiedzi są uporządkowane według głębokości zależności: komórki, które można wydedukować natychmiast, pojawiają się jako pierwsze, a komórki wymagające długich łańcuchów wcześniejszych dedukcji — jako ostatnie.
Końcowa zagadka jest pakowana ze wszystkimi danymi potrzebnymi grze: metadanymi, zestawem wskazówek, sekwencją podpowiedzi i oceną trudności.
Solver: jak udowadniana jest unikalność
Sercem potoku jest Google OR-Tools CP-SAT — solver programowania z ograniczeniami, który łączy propagację ograniczeń, programowanie całkowitoliczbowe i rozwiązywanie SAT.
Jak zagadka staje się problemem matematycznym
Każda komórka na siatce jest modelowana jako zmienna boolowska: Podejrzany (1) lub Niewinny (0). Każda wskazówka staje się jednym lub wieloma ograniczeniami matematycznymi nałożonymi na te zmienne.
Na przykład:
- „W wierszu 3 jest dokładnie 2 podejrzanych" staje się:
cell[3,0] + cell[3,1] + cell[3,2] + cell[3,3] = 2 - „Wszyscy podejrzani w kolumnie A są połączeni" staje się: ograniczenie łączności zapewniające, że podejrzane komórki w kolumnie A tworzą ciągły łańcuch bez przerw.
- „Wiersz 1 ma więcej podejrzanych niż kolumna B" staje się:
sum(row_1) > sum(col_B)
Jak weryfikowana jest unikalność
Po złożeniu zestawu wskazówek generator zadaje CP-SAT precyzyjne pytanie: „Czy przy tych ograniczeniach istnieje więcej niż jedno prawidłowe przypisanie?"
CP-SAT nie znajduje po prostu jednego rozwiązania — potrafi wyliczyć wszystkie rozwiązania. Jeśli solver znajduje dokładnie jedno, zagadka jest prawidłowa. Jeśli znajduje dwa lub więcej, generator wraca do Fazy 3 i dodaje kolejną wskazówkę.
To jest formalny dowód, nie heurystyka. CP-SAT wyczerpująco przeszukuje całą przestrzeń rozwiązań. Jeśli stwierdza, że jest jedno rozwiązanie, to jest dokładnie jedno — kropka.
Dlaczego nie wystarczy sprawdzić wszystkich możliwości metodą brute-force?
Siatka 5×5 ma 25 komórek, każda z 2 możliwymi wartościami. To 2²⁵ = 33 miliony możliwych plansz. Sprawdzanie ich wszystkich metodą brute-force jest powolne i nie skaluje się.
CP-SAT jest dramatycznie szybszy dzięki propagacji ograniczeń: gdy wskazówka mówi „wiersz 3 ma dokładnie 2 podejrzanych", solver natychmiast redukuje przestrzeń poszukiwań dla każdej komórki w wierszu 3, nie sprawdzając każdej kombinacji osobno. Złożone wskazówki potęgują ten efekt. W praktyce CP-SAT udowadnia unikalność dla zagadki 5×5 w milisekundach.
Co mogłoby pójść nie tak (i jak temu zapobiegamy)
„Co jeśli wskazówka jest niejednoznaczna?"
Każdy typ wskazówki ma formalną definicję matematyczną. „Sąsiedzi" zawsze oznaczają do 8 otaczających komórek, łącznie z przekątnymi. „Połączone" zawsze oznacza ciągły łańcuch przylegających komórek. „Między" zawsze oznacza komórki w tym samym wierszu lub kolumnie, z wyłączeniem punktów końcowych.
Te definicje są wbudowane bezpośrednio w model ograniczeń — nie ma etapu interpretacji języka naturalnego, na którym mogłaby wkraść się dwuznaczność. Dostępna w grze Szczegóły wyjaśniające pokazują graczom dokładnie, co oznacza każde słowo kluczowe przestrzenne.
„Co jeśli solver ma błąd?"
Solver CP-SAT to dobrze przetestowane, szeroko stosowane narzędzie utrzymywane przez zespół optymalizacji Google. Ale nie polegamy wyłącznie na zaufaniu. Każda wygenerowana zagadka jest niezależnie weryfikowana:
- Automatyczny solver próbuje rozwiązać każdą zagadkę krok po kroku, symulując ludzkiego gracza. Jeśli nie może osiągnąć kompletnego rozwiązania wyłącznie przez logiczną dedukcję, zagadka jest odrzucana.
- Kontrole poprawności podpowiedzi weryfikują, czy każda podpowiedź w sekwencji jest logicznie poprawna — że podpowiadana komórka jest rzeczywiście dedukowalna ze wskazówek i wcześniej odsłoniętych komórek, a nie z ukrytych informacji.
„Co jeśli generowanie wskazówek pominie przypadki brzegowe?"
Każdy typ wskazówki ma formalną funkcję ewaluacji testowaną na znanych konfiguracjach zagadek. Faza generowania puli wskazówek uwzględnia tylko wskazówki, które ewaluują się jako prawdziwe na faktycznym rozwiązaniu — wskazówka fałszywa na rozwiązaniu nigdy nie może pojawić się w zagadce.
Rezultat
Kiedy otwierasz zagadkę Griductive, oto co już się wydarzyło:
- Wygenerowano losowe rozwiązanie.
- Tysiące kandydujących wskazówek zostało zewaluowanych.
- Wybrano minimalny, nieredundantny podzbiór.
- Formalny solver udowodnił, że dokładnie jedno rozwiązanie spełnia te wskazówki.
- Automatyczny solver niezależnie zweryfikował, że zagadka jest rozwiązywalna wyłącznie przez czystą dedukcję.
- Obliczono ocenę trudności i wygenerowano sekwencję podpowiedzi.
Każda zagadka, każdego dnia, we wszystkich czterech rozmiarach siatki. Bez wyjątków.
Obietnica jest dotrzymana: jeśli utknąłeś, jest wskazówka, której jeszcze w pełni nie wykorzystałeś. Jeśli uważasz, że dwie odpowiedzi są możliwe, przeczytaj wskazówki jeszcze raz — logika to rozstrzygnie. A jeśli chcesz dowodu, Graf logiczny pokaże ci dokładny łańcuch dedukcji od wskazówek do rozwiązania.
Co dalej: wskazówki, które opowiadają historię
Obecnie wskazówki w Griductive brzmią jak precyzyjne stwierdzenia logiczne — jasne i jednoznaczne, ale trzeba przyznać, trochę kliniczne. „W wierszu 3 jest dokładnie 2 podejrzanych" spełnia swoje zadanie, ale nie sprawia, że czujesz się jak detektyw pracujący nad sprawą.
Aktywnie pracujemy nad zmianą tego stanu rzeczy. Celem jest zróżnicowanie sposobu wyrażania wskazówek — wplecenie tematycznego kolorytu przy zachowaniu tej samej logicznej precyzji. Wyobraź sobie wskazówki powiązane ze świątecznymi wydarzeniami lub sformułowane jako zeznania świadków z konkretnego miejsca zbrodni. Zamiast sterylnej formuły czytałbyś coś, co brzmi jak prawdziwy dowód z dochodzenia.
Kluczowe ograniczenie się nie zmieniło: każda wskazówka musi pozostać spójna, jednoznaczna i formalnie weryfikowalna. Solver nie dba o to, czy wskazówka brzmi jak podręcznik matematyki, czy jak powieść kryminalna w stylu noir — liczy się wyłącznie treść logiczna. To rozdzielenie sprawia, że bogatsze formy wyrazu są możliwe bez kompromisów w zakresie poprawności.
Te same gwarancje. Ten sam rygor. Ale zagadki, które wyglądają mniej jak równania, a bardziej jak sprawy warte rozwiązania.
Bez zgadywania. Bez szczęścia. Z matematyczną gwarancją.