Informaticienii și matematicienii de la Universitatea Carnegie Mellon au rezolvat ultima parte complicată din conjectura lui Keller, o problemă geometrică pe care oamenii de știință au încercat să o soluționeze timp de 90 de ani.

Structurând problema ca ceea ce informaticienii numesc o problemă de satisfacție, cercetătorii au găsit soluția timp de patru luni de programare și doar 30 de minute de calcul folosind un grup de computere.

„Am fost foarte fericit când am rezolvat-o, dar apoi am fost puțin trist că problema a dispărut”, a spus John Mackey, profesor didactic în cadrul Departamentului de Informatică (CSD) și al Departamentului de Științe Matematice care a studiat conjectura lui Keller timp de 30 de ani. “Dar apoi m-am simțit din nou fericit. Există doar acest sentiment de satisfacție.”

Soluția a fost un alt succes pentru o abordarea inițiată de Marijn Heule, profesor de informatică care s-a alăturat CSD în august anul trecut. Heule a folosit un rezolvator SAT – un program de calculator care folosește logica propozițională pentru a rezolva probleme de satisfacție (SAT) – pentru a acoperi mai multe provocări matematice, inclusiv problema triplelor Pitagoreice și numărul Schur 5. „Problema a intrigat mulți oameni de zeci de ani, aproape un secol”, a spus Heule despre conjectura lui Keller. “Aceasta este într-adevăr un exemplu a ceea ce se poate face acum, care nu era posibil anterior.”

Conjectura, propusă de matematicianul german Eduard Ott-Heinrich Keller, are de-a face cu placarea – în special, cum să acoperiți o zonă cu plăci de dimensiuni egale fără goluri sau suprapuneri. Conjectura este că cel puțin două dintre plăci vor trebui să împartă o margine și că acest lucru este adevărat pentru spațiile de fiecare dimensiune. Este ușor să demonstrezi că este adevărat pentru plăcile bidimensionale și cuburi tridimensionale. Începând din 1940, conjectura se dovedise adevărată pentru toate dimensiunile până la șase. Cu toate acestea, în 1990, matematicienii au demonstrat că nu funcționează la dimensiunea 10 sau mai mare.

CITEȘTE:  TRAPPIST-1 ar putea avea prea multă apă ca să susțină viață

Atunci conjectura lui Keller a capturat imaginația lui Mackey, pe atunci student la Universitatea din Hawaii. Cu un birou lângă grupul de calcul al universității, el a fost intrigat, deoarece problema putea fi translată, folosind teoria discretă a graficelor, într-o formă pe care computerele ar putea să o studieze. În această formă, numită grafic Keller, cercetătorii ar putea căuta „clici” – subseturi de elemente care se conectează fără a împărtăși o față, respingând astfel conjectura.

În 2002, Mackey a făcut exact asta, descoperind o clică în dimensiunea opt. Procedând astfel, el a demonstrat că conjectura eșuează la acea dimensiune și, prin extensie, la dimensiunea nouă. Acest lucru a lăsat conjectura nerezolvată pentru dimensiunea șapte.

„M-am gândit în sinea mea, poate putem folosi tehnica SAT”, și-a amintit Mackey. În scurt timp, a început să discute despre modul de utilizare a soluției SAT pe conjectura lui Keller cu Heule și Joshua Brakensiek, un specialist în științe matematice și informatică, care urmează acum un doctorat în informatică la Universitatea Stanford.

Un rezolvator SAT necesită structurarea problemei utilizând o formulă propozițională – (A sau nu B) și (B sau C) etc. – astfel încât rezolvătorul să poată examina toate variabilele posibile pentru combinații care vor satisface toate condițiile. „Există multe modalități de a face aceste translări, iar calitatea translării îți favorizează sau încurcă de obicei capacitatea de a rezolva această problemă geometrică”, a spus Heule. Cu o experiență de 15 ani, Heule este priceput la efectuarea acestor translări. Unul dintre obiectivele sale de cercetare este de a dezvolta un raționament automat, astfel încât această translare să poată fi realizată automat, permițând mai multor oameni să folosească aceste instrumente pentru problemele lor.

CITEȘTE:  NASA planifică căutarea vieții extraterestre pe satelitul lui Jupiter

Chiar și cu o translare de înaltă calitate, numărul combinațiilor care trebuie verificate în dimensiunea a șaptea a fost uluitor – un număr cu 324 de cifre – cu o soluție nevăzută la prima vedere chiar și cu un supercomputer. Dar Heule și ceilalți au aplicat o serie de trucuri pentru a reduce dimensiunea problemei. De exemplu, dacă o configurație de date s-a dovedit ineficientă, ar putea respinge automat alte combinații care se bazau pe ea. Și întrucât o mare parte a datelor erau simetrice, programul ar putea exclude imaginile oglindă ale unei configurații dacă ar ajunge la un punct mort într-un singur aranjament pentru a soluționa această problemă geometrică.

Folosind aceste tehnici, și-au redus căutarea la aproximativ un miliard de configurații. În acest efort li s-a alăturat un doctorand David Narvaez, student la Institutul de Tehnologie Rochester. Odată ce și-au rulat codul pe un grup de 40 de computere, au avut în cele din urmă un răspuns: conjectura este adevărată în dimensiunea a șaptea. “Motivul pentru care am reușit este că John are decenii de experiență și o perspectivă asupra acestei probleme și am putut să o transformăm într-o căutare generată de computer”, a spus Heule.

Dovada rezultatului la această problemă geometrică este complet calculată de computer, a spus Heule, spre deosebire de multe publicații care combină porțiuni verificate de computer ale unei dovezi cu scrieri manuale ale altor porțiuni. Acest lucru face dificilă înțelegerea cititorilor, a remarcat el. Dovada computerizată pentru soluția Keller include toate aspectele soluției, inclusiv o porțiune de simetrie contribuită de Narvaez, a subliniat Heule, astfel încât niciun aspect al dovezii nu trebuie să se bazeze pe efortul manual.

CITEȘTE:  Modulul gonflabil NASA a rezistat deja un an în spațiu

“Putem avea încredere reală în corectitudinea acestui rezultat”, a spus el. O lucrare care descrie rezoluția lui Heule, Mackey, Brakensiek și Narvaez a câștigat un premiu pentru cea mai bună lucrare la Conferința internațională privind raționamentul automatizat din iunie. Rezolvarea presupunerii lui Keller are aplicații practice, a spus Mackey. Acele clici pe care oamenii de știință le caută pentru a respinge presupunerea sunt utile în generarea de coduri neliniare care pot face transmisia datelor mai rapidă. Rezolvatorul SAT poate fi astfel utilizat pentru a găsi coduri neliniare cu dimensiuni mai mari decât anterior.

astrofeed patreon

via: [Phys.org]