Riešenie kombinatorických problémov pomocou SAT-solverov

Abstrakt: 

Počas posledných 20 rokov došlo k významnému pokroku pri praktickom riešení problému splniteľnosti. Využijeme moderné SAT-solvery na analýzu štruktúry zaujímavých kubických grafov, verifikáciu viacerých významných hypotéz a hľadanie vhodných konštrukčných blokov potrebných pri vytváraní kubických grafov s danými parametrami (cyklická súvislosť, nepárnosť, cirkulárny chromatický index, obvod, circumference apod.)

Odbor: 
Teoretická informatika
Vedecká časť: 

Ukazuje sa, že redukcia grafových farbení a súvisiacich kombinatorických problémov na splniteľnosť boolovských formúl a následné použitie moderných SAT-solverov je v súčasnosti najefektívnejší spôsob ako tieto problémy riešiť.

Cieľom projektu je využiť SAT-solvery pri riešení rôznych problémov súvisiacich s hranovými farbeniami kubických grafov, a to najmä:
(1) určovanie cirkulárneho chromatického indexu kubických grafov, napr. pre malé grafy s obvodom 6;
(2) konštrukcie čo najmenších snarkov s nepárnosťou 4 a 6;
(3) konštrukcie kubických grafov s danou cyklickou súvislosťou bez dlhých kružníc;
(4) analýza štruktúry nekritických snarkov na 38 vrcholoch;
(5) farbenie kubických grafov konfiguráciami.

Mnoho problémov bolo vyriešených tak, že najprv bol hrubou silou objavený jeden exemplár zaujímavého grafu a ten bol následne využitý pri konštrukcii nekonečnej triedy grafov s požadovanou vlastnosťou. Alternatívne, mnohé naše konštrukcie závisia od dostupnosti vhodných konštrukčných blokov, ktoré možno hľadať v existujúcej databáze so stovkami miliónov grafov, to však vyžaduje značnú výpočtovú silu. Pre testovanie mnohých vlastností je využitie SAT-solvera jediná dostupná možnosť. Takto sme postupovali (okrem využitia SAT solverov) aj pri väčšine z nižšie uvedených výsledkov.

Relevantné publikácie:
D. Kráľ, E. Máčajová, J. Mazák, J.-S. Sereni, Circular
edge-colourings of cubic graphs with girth six, Journal of
Combinatorial Theory Series B 100 (2010), 351--358.

R. Lukoťka, J. Mazák, Cubic graphs with given circular chromatic
index, SIAM J. Discrete Math. 24 (3) (2010), 1091--1103.

R. Lukoťka, E. Máčajová, J. Mazák, M. Škoviera, Circuits of length
five in 2-factors of cubic graphs, Disc. Math. 312 (2012), 2131--2134.

R. Lukot'ka, E. Máčajová, J. Mazák, M. Škoviera, Small snarks with
large oddness, Electron. J Combin. 22 (1) (2015), #P1.51.

E. Máčajová, J. Mazák, Cubic Graphs with Large Circumference
Deficit, J. Graph Theory 82 (4) (2016), 433–440.

Socioekonomický a technologický dopad: 

Plánujeme identifikovať ťažké inštancie problému splniteľnosti, ktoré pochádzajú z hranových farbení, a zverejniť benchmarkové sady takýchto inštancií. Následne popísať, ktoré z dostupných SAT solverov sú pre riešenie problémov nášho typu najvhodnejšie, a akým spôsobom ich treba konfigurovať, čo ušetrí výskumníkom množstvo práce v budúcnosti. Identifikované ťažké inštancie môžu viesť k všeobecnému zlepšeniu výkonnosti SAT-solverov, vrátane ich využitia v priemyselných aplikáciách.

Technická časť: 

Je ťažké toto špecifikovať dopredu, pretože zatiaľ nevieme, či využitie masívnej paralelizácie SAT solverom naozaj pomáha --- z predbežných pokusov na 4-jadrových procesoroch sa zdá, že ani nie, a že lepšou stratégiou je rozdeliť vstupné grafy na veľa malých sád a experimenty na nich robiť nezávisle. Do úvahy prichádzajú najmä SAT solvery zo súťaže 2018: http://sat2018.forsyte.tuwien.ac.at/solvers/
V princípe si teda väčšinu softvéru skompilujeme sami (vrátane grafových algoritmov), možno budeme mať záujem o Gurobi alebo nejaký iný ILP solver.

V závislosti od dostupného strojového času vieme vyskúšať viac vecí, resp. na o čosi väčších grafoch, čo významne zvyšuje šance na úspech pri hľadaní grafov s danými vlastnosťami. Povedzme 1 rok strojového času (pár týždňov x 1 node with 32 cores) vieme určite dobre využiť aj na veci, ktoré už máme naprogramované, a podľa toho, čo z toho vyjde, sa rozhodneme, čo programovať a skúšať ďalej.

Odhad potrebného diskového priestoru je 50 až 100 GB (najväčšia dostupná sada grafov, ktoré chceme využiť ako vstup, má veľkosť zhruba 20 GB).

Sieťovú komunikáciu počas samotných výpočtov budeme využívať len minimálne.

Prepojenie s grantovými úlohami: 
APVV-15-0220, VEGA 1/0876/16, špičkový tím (vedúci prof. Martin Škoviera)
Spolufinancovanie: 
0.00
Výstupy: 
none