Ročníkový projekt

Automatizované riešenie úloh o dláždení polyominami

Študent: Dávid Mišiak
Email: misiak3@uniba.sk

Školiteľ: doc. RNDr. Ján Mazák, PhD.
Email: mazak@dcs.fmph.uniba.sk

Popis

Rovinný útvar, ktorý dostaneme spojením niekoľkých rovnakých štvorčekov pozdĺž ich hrán, je známy ako polyomino ("zovšeobecnené domino"). V zábavnej matematike sa stretávame s triedou úloh, kde má riešiteľ dokázať alebo vyvrátiť existenciu dláždenia zadanej štvorčekovej mriežky zadanými polyominami, napríklad:

Dá sa mriežka 10 × 10 vydláždiť 25 tetrominami 4 × 1?

Cieľom projektu je vytvoriť program, ktorý bude vedieť riešiť tento typ úloh (teda nájsť dláždenie alebo dokázať, že neexistuje). Súčasťou projektu bude definovanie vhodných vstupných a výstupných formátov, implementácia viacerých metód riešenia (backtracking, SAT solver, ...) a ich porovnanie.

Repozitár

Zimný semester - plán

• Vybrať programovací jazyk.
  Vybral som C++, kvôli výkonu, dobrej interoperabilite so SAT solvermi a tiež preto, že si chcem vyskúšať spraviť nejaký väčší projekt v tomto jazyku.
• Vybrať vhodné vývojové nástroje, oboznámiť sa s nimi a vytvoriť kostru projektu.
  Snažil som sa vybrať populárne nástroje a spojiť ich do robustnej kostry. Rozhodol som sa pre stack CMake, Conan, ClangFormat, Cppcheck, Catch2, GDB, Gitlab CI.
• Vytvoriť základ CLI.
  Použil som knižnice CLI11 a rang (terminal colors) a premyslel si približnú štruktúru UI.
• Definovať formát vstupu, naprogramovať parser.
  Momentálne sú k dispozícii tri rôzne vstupné formáty (viď README.md). V letnom semestri pribudne štvrtý.
• Naprogramovať jednoduchý solver backend - naivný backtracking.
  Je naprogramovaný a mal by fungovať. Podaril sa celkom stručný.
• Napísať nejaké testy.
  Aké-také testy má zatiaľ iba jedna trieda. Je možné, že doterajší kód obsahuje nepekné bugy - v letnom semestri teda určite začnem písaním testov.

Zimný semester - výstupy

Letný semester - plán

• Dopísať testy (a prípadne opraviť bugy, ktoré odhalia).
  Dopísané, opravené.
• Generovať grafické výstupy - obrázok s riešením.
  Generuje sa SVG (a nejaká podoba riešenia sa píše aj na stdout).
• Dorobiť parser na tvary zadané obvodom (napr. DDRRULUL).
  Hotový.
• Naprogramovať SAT backend.
  Spravil som čo najjednoduchší transformátor z problému dláždenia na problém splniteľnosti. Integroval som až dva SAT solvery - CaDiCaL a CryptoMiniSat (pre porovnanie).
• Spraviť jednoduché porovnanie výkonu backendov.
  Použil som knižnicu Benchmark od Googlu, výsledky sú v reporte.

Letný semester - výstupy