A Conway 99 probléma megoldásának keresése SAT solver alkalmazásával

Tervezze meg a John Conway által 2014-ben meghirdetett, (99, 14, 1, 2) paraméterű erősen reguláris gráfhoz tartozó megoldatlan probléma logikai kielégíthetőségi (SAT) reprezentációját.
Mutassa be az erősen reguláris gráfhoz tartozó problémát és a gráf már ismert tulajdonságait. Ismertesse a logikai kielégíthetőségi problémát, annak elméleti és gyakorlati megoldhatóságát, továbbá a SAT reprezentációban rejlő kihívásokat és azok lehetséges megoldásait.
A különböző reprezentációk előállítását valósítsa meg C++ programozási nyelven. Az elkészült SAT problémákat elemezze és vonjon le következtetést arra vonatkozólag, hogy melyik reprezentáció lehet a legalkalmasabb a probléma megoldására.

A diplomamunkának tartalmaznia kell:

• a feladat leírását,
• a szakirodalom alapján megismert hasonló módszerek, rendszerek ismertetését és értékelését,
• a választott módszer bemutatását,
• a megvalósítandó feladat tervét,
• a felhasználói leírást,
• az elért eredmények értékelését,
• a továbbfejlesztési lehetőségeket,
• a dokumentációt, a programot, a szükséges input adatokat, valamint a rendszert bemutató prezentációt.