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