Kombinatorikai feladatok megoldás SAT-solverrel

Témavezető: Damásdi Gábor
ELTE TTK, Számítógéptudományi Tanszék
email: damasdigabor@student.elte.hu

Projekt leírás

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ó.

Előfeltételek

Alapvető programozási ismeretek, lehetőleg Python.

Hivatkozások

Chromatic numbers of integer distance graphs, Arnfried Kemnitz, Massimiliano Marangio, Diskrete Mathematik, Technische Universitat Braunschweig, Pockelsstr. 14, D-38106 Braunschweig, Germany

Armin Biere, Marijn J.H. Heule, Hans van Maaren, and Toby Walsh (2021). Handbook of Satisfiability, Second Edition.

Korábbi hallgatók