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

Wojciech Karpiel dd59bb76ab rażąca i niewybaczalna literówka. Idę popełnić sudoku 2 years ago
.gitignore 2218b6df61 Sprzątanie w trakcie 2 years ago
GrupaPrzemiennaModulo.v 1dd2366228 uładnić dowody o liczbach i życiu 2 years ago
Makefile 2218b6df61 Sprzątanie w trakcie 2 years ago
README.md dd59bb76ab rażąca i niewybaczalna literówka. Idę popełnić sudoku 2 years ago
Rozwiazanie.md 5354860c82 naprawa CZYTAJMNIE 2 years ago
Wiezniowie.v 87560edbaa pozdrawiam ludzi, którzy to czytają 2 years ago

README.md

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