Dankó Dorottya: Kombinatorikai feladatok megoldása SAT-solverrel

Önálló projekt, szakmai gyakorlat II

2022/23 II. félév

Témavezető:
Damásdi Gábor (ELTE TTK, Számítógéptudományi Tanszék)

Sok kombinatorikai kérdés megfogalmazható logikai formulákkal, és ezen logikai formulák megoldhatóak SAT-solverek segítségével. Pl sudoku, 9 királynő, gárfszínezés, stb... A kutatás során körbejárunk néhány ismeret eredményt és megpróbáljuk sat-solverek segítségével reprodukálini/bővíteni ezeket.

Egy lehetséges probléma a következő: Adott néhány egész szám, és szeretnénk az egész számok halmazát kiszínezni úgy, hogy ha két szám különbsége a megadott számok között van, akkor nem lehetnek azonos színűek. Legalább hány színre van ekkor szükség? A válasz természetesen a megadott számoktól függ, de sok esetben megválaszolható.