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
|
%!s(int64=3) %!d(string=hai) anos | |
|---|---|---|
| .gitignore | %!s(int64=3) %!d(string=hai) anos | |
| GrupaPrzemiennaModulo.v | %!s(int64=3) %!d(string=hai) anos | |
| Makefile | %!s(int64=3) %!d(string=hai) anos | |
| README.md | %!s(int64=3) %!d(string=hai) anos | |
| Rozwiazanie.md | %!s(int64=3) %!d(string=hai) anos | |
| Wiezniowie.v | %!s(int64=3) %!d(string=hai) anos |
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:
- Naczelnik da więźniom kilka dni do namysłu i ustalenia strategii
- Gdy czas do namysłu się skończy, więźniowie dostaną zakaz jakiejkolwiek komunikacji między sobą
- Naczelnik napisze na czole każdego z więźniów liczbę od 0 do N-1, liczby mogą się powtarzać
- 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
- Więźniowie będą po kolei szeptali na ucho naczelnikowi domniemaną odpowiedź na pytanie: "Jaką liczbę masz na czole?"
- 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ą):
- Coq (8.13.2)
- Mathematical Components: ssreflect, algebra (1.12.0)
Kompilacja: make