SAT-solvery

Prowadzący: Krzysztof Zając


Kategorie:
informatyka

Zapisz się

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