SAT-solvery

Opis

Rozważmy problemy takie jak:

1. rozwiązywanie sudoku,
2. problem 8 hetmanów,
3. znajdowanie stanów Gry w Życie, które spełniają zadane warunki,
4. planowanie projektów,
5. gra w Sapera.

Okazuje się, że mają jedną wspólną cechę: można je zapisać w formie wyrażenia logicznego (takiego jak np. p i nieprawda, że q) i poszukiwać rozwiązania przez szukanie wartości zmiennych, dla których to wyrażenie jest prawdziwe.

W trakcie warsztatów poznacie narzędzia (SAT-solvery), które radzą sobie z takimi problemami zaskakująco dobrze, nawet mając do czynienia z dziesiątkami tysięcy zmiennych. W wielu przypadkach (na przykład Sudoku) wystarczy przepisać treść zadania w formie zrozumiałej dla
SAT-solvera, aby w ciągu poniżej sekundy uzyskać wynik.

Warsztaty będą miały formę praktycznych zajęć, na których będziecie mieli okazję zaimplementować rozwiązanie wybranych problemów przy użyciu SAT-solvera.

Wymagania

Podstawowa umiejętność programowania w dowolnym języku.

Inne

Rozwiązanie zadań przesyłajcie przez stronę (a nie prowadzącym na maila).

W razie pytań (np. dotyczących zajęć, zadań kwalifikacyjnych) piszcie na krzysztof.zajac2 (at) gmail.com