Original English version: http://www.cs.cmu.edu/~bryant/boolean/macgregor.html
Randal E. Bryant
I april 1975 utgaven av Vitenskapelig amerikansk, Martin Gardner, i sin spalte “Matematiske spill” publisert en liste over hva han hevdet var 6 store matematiske oppdagelser av 1974 at “for en eller annen grunn ble tilsidesatt rapportert til både det vitenskapelige samfunnet og publikum for øvrig.”den ene var en plan, 110-node graf, tilskrevet William McGregor av Wappingers faller, New York, som han hevdet ikke kunne være farget med mindre enn 5 farger, og dermed motbevise det som ennå uprøvd formodning om at 4 fargene var tilstrekkelig til å farge et hvilket som helst plan graf. Hva mange lesere setter pris på ikke var måneden for offentliggjøring av saken. Mer om historien kan bli funnet her.
Her er grafen, tegnet som et kart
Å prøve å kode mulig fargelegging av denne grafen som en BDD er egentlig ikke mulig. Jeg anslår at det vil ta over en milliard noder (siden et minkutt av grafen er 20 noder bredt, og BDD vil måtte eksponentielt kode for nesten alle kombinasjoner av farger for disse nodene.)
Graffarging som et SAT-problem
På den annen side er det ganske mulig å fargelegge grafen med en Boolean satisfiability (SAT) løser. Løseren trenger bare å finne en mulig løsning, og den står ikke overfor den skremmende oppgaven å kode alle mulige fargelegninger. Her er en farging som genereres av ZChaff løser gang på mindre enn ett sekund på en bærbar datamaskin
Sjekk ut følgende Youtube-video som viser hvordan dette søket fortsetter:
Det er også mulig å tvinge løsemidlet til å generere en “balansert” fargelegging, ved å kreve at den finner en løsning ved bruk av to farger (grønn og blå) 27 ganger og to farger (rød og gul) 28 ganger.
SAT-løsere kan også brukes til å løse optimaliseringsproblemer ved å utføre en serie samtaler til løserne for å gjøre binært søk på objektivfunksjonen. Hvis vi ber løseren om å finne en fargelegging som først minimerer antall noder farget grønt, så minimerer antallet farget blått, og deretter rødt, får vi en fargelegging med bare 7 grønne noder, 34 blå og røde og 35 gule.
Basert på ytterligere eksperimenter, kan vi opplyse at denne løsningen har frem til farger, har unike egenskaper:
- Det er den eneste fargeleggingen der en farge brukes mest 7 ganger.
- Det er den eneste fargeleggingen der en farge brukes minst 35 ganger.
Randal E. Bryant