README.md 1.6 KB

Więźniowie

Repo zawiera rozwiązanie i dowód formalny poprawności rozwiązania zagadki logicznej o więźniach

Treść zagadki

W więzieniu było N więźniów. Naczelnik ogłosił więźniom, że mają szansę odzyskać wolność, jeśli sprostają wyzwaniu. Naczelnik przedstawił więźniom następujące zasady wyzwania:

  1. Naczelnik da więźniom kilka dni do namysłu i ustalenia strategii
  2. Gdy czas do namysłu się skończy, więźniowie dostaną zakaz jakiejkolwiek komunikacji między sobą
  3. Naczelnik napisze na czole każdego z więźniów liczbę od 0 do N-1, liczby mogą się powtarzać
  4. Każdy z więźniów będzie widział liczby na czołach pozostałych współwięźniów, ale nie będzie widział swojej
  5. Więźniowie będą po kolei szeptali na ucho naczelnikowi domniemaną odpowiedź na pytanie: "Jaką liczbę masz na czole?"
  6. Jeśli co najmniej jeden z więźniów zgadnie, wszyscy odzyskują wolność

Jaka jest optymalna strategia dla więźniów? W jakich przypadkach zadziała, a w jakich nie?

Źródło zagadki: nie wiem, znalazłem tą zagadkę na zkserowanym fragmencie kartki w formie bajki o Pawle i Gawle. Jeśli ktoś zna źródło to proszę o podanie.

Rozwiązanie

Tutaj jest opis słowno-muzyczny, a dowód formalny w pliku Wiezniowie.v.

Szczegóły techniczne

Wymagane zależności (w nawiasie podano wersje, które na pewno działają):

Kompilacja: make