Vaším úkolem bude vytvořit systém pro řešení zadaného výpočetního problému za použití SAT solveru. Budeme řešit rozhodovací problém (odpověď ano/ne), jde-li o optimalizační problém, řešte jeho rozhodovací variantu: “Má daná instance řešení, jehož objektivní funkce má alespoň/nejvýše danou hodnotu?”
Neurčí-li váš cvičící jinak:
K řešení použijte programovací jazyk Python 3 a SAT solver Glucose 4.2. Nepoužívejte žádné knihovny, které umí převádět formule do CNF apod.
Naprogramujte skript, který:
K řešení přiložte několik instancí, a to alespoň:
Dále musí být součástí řešení soubor README.md se stručnou dokumentací obsahující:
Při řešení musíte postupovat zcela samostatně. Není dovoleno řešení konzultovat s žádnou inteligencí kromě cvičícího. Můžete vyhledávat doplňující informace o daném problému (např. zajímavé instance nebo není-li vám jasné zadání problému), ale nesmí se týkat jeho zakódování do CNF nebo použití SAT solveru k jeho řešení. Nesmíte také číst žádný kód řešící daný (nebo příbuzný) problém. V případě nejasností jak postupovat se obraťte na cvičícího, který vám poskytne pomoc nebo nápovědu.
Pro inspiraci si prohlédněte ukázkové řešení (.zip) problému 15 Puzzle, které laskavě vypracoval Dr. Jirka Švancara (kterému tímto děkuji).
Každý student v rámci jedné skupiny cvičení bude řešit jiný problém. Můžete si vybírat ze seznamu níže, nebo i navrhnout vlastní problém, který vás zajímá: V tom případě popište o jaký problém jde a proč vás zajímá (podléhá schválení cvičícím, musí být rozumně obtížný - proto raději uveďte i preference problémů ze seznamu).
Neurčí-li váš cvičící jinak:
Vaše preference pošlete cvičícímu emailem. Můžete napsat libovolné množství problémů, každý název problému na samostatný řádek dle pořadí preferencí. V případě, že o váš nejvíce preferovaný problém bude mít zájem více studentů, bude přidělen jednomu náhodně zvolenému, a dále se bude postupovat níže ve vašem seznamu preferencí. Bezproblémovým studentům budou nakonec přiřazeny nepřiřazené problémy náhodně.
Neurčí-li váš cvičící jinak:
Hotový projekt odevzdejte buď jako link na veřejný GitHub nebo GitLab repozitář, nebo v .zip souboru, jedno z toho zašlete emailem cvičícímu.