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