Coloring the MacGregor Graph [Romanian]

Original in English by Randy Bryant

Colorînd graficul lui MacGregor

În aprilie anului 1975, într-un număr a ziarului Scientific American, Martin Gardner, în coloana lui "Jocuri matematice" ("Mathematical Games") a publicat o listă de ceea ce el a numit 6 descoperiri majore matematice din 1974, care "pentru un motiv sau altul au fost exprimate inadecvat atât în comunitatea ştiinţifică cît şi publicului larg”.  Un punct din această listă reprezenta un plan, graficul din 110 noduri, atribuit lui William MacGregor din Wappingers Falls, New York, care a afirmat că el nu a putut fi colorat cu mai puţin de 5 culori, ceea ce neagă astfel conjectura ca nu e încă dovedit că 4 culori au fost suficiente pentru orice culorare a graficului plan. Ceea ce mulţi cititori nu au apreciat a fost tema generală a acestei ediții ziarului. Mai multe despre această povestire poate fi găsit aici – here.

Aici este graficul, tras ca o hartă

macgregor

Încercați de a codifica colorare posibilă de acest grafic ca BDD, care nu este cu adevărat posibil. Estimez că acesta aș avea nevoie mai bine peste un miliard de noduri (din moment ce minimal graficul e tăiat cu 20 de noduri largime, şi BDD ar trebui să codifice exponenţial aproape toate combinaţiile de culori pentru aceste noduri).

Graficul de colorat ca o problemă SAT

Pe de altă parte, colorarea graficului cu o satisfiabilitate booleană (SAT) rezolvitorului este destul de posibilă. Rezolvatorul are nevoie să gasească doar o soluţie posibilă, şi aşa că nu se confruntă cu sarcină dificilă de codificare a toatelor coloranţi posibili. Aici este o colorare generată de rezolvatorul ZChaff solver  care se execută în conformitate cu o secundă pe un laptop.

macgregor

Priviți următorul video Youtube care arată modul în care această căutare se execută:

Este de asemenea posibil de a forța rezolvatorul pentru a genera o colorare "echilibrată", prin solicitarea ca aceasta să găsească o soluţie folosind două culori (verde şi albastru), de 27 de ori şi de două culori (roşu şi galben) de 28 de ori.

macgregor

Rezolvatorii SAT pot fi, de asemenea, folosiți pentru a rezolva probleme de optimizare, prin efectuarea unei serii de apeluri la rezolvarea căutării binare cu privire la funcţia obiectivă. Dacă cerem rezolvatorul să găsească o colorare care minimizează mai întâi numărul de noduri colorate verzi, apoi minimizează numărul de coloraturi albastru, şi apoi roşu, vom obţine o colorare cu doar 7 noduri verzi, 34 albaștri şi roşii, şi 35 galbene.

inunbalance

Bazat pe experimente viitoare, putem afirma că, până la atribuirea culorilor, această soluţie are proprietăţi unice:

  • Colorarea se produce numai în cazul în care o culoare este folosită la cele mai multe de 7 ori.

  • Colorarea se produce numai în cazul în care o culoare este utilizată cel puţin de 35 de ori. 

ok ok