Problem med stympat schackbräde
det stympade schackbrädet är ett kakelpussel som ställdes av Max Black 1946 som frågar:
standardschackbräde 8×8 (eller schackbräde ) har två diagonalt motsatta hörn borttagna, vilket lämnar 62 rutor. Är det möjligt att placera 31 dominobrickor i storleken 2×1 för att täcka alla dessa rutor?
Det är ett omöjligt pussel : det finns ingen dominoplatta som uppfyller dessa villkor. Ett bevis på dess omöjlighet använder det faktum att, med hörnen borttagna, har schackbrädet 32 rutor av en färg och 30 av den andra, men varje domino måste täcka lika många rutor av varje färg. Mer generellt, om två rutor tas bort från schackbrädet, kan resten läggas ihop med dominobrickor om och endast om de borttagna rutor är av olika färg. Detta problem har använts som ett testfall för automatiserat resonemang , kreativitet och matematikens filosofi .
Historia
Problemet med det stympade schackbrädet är ett exempel på dominobeläggning av rutnät och polyominoer , även känd som "dimermodeller", en allmän klass av problem vars studier i statistisk mekanik dateras till Ralph H. Fowlers och George Stanley Rushbrookes arbete 1937. Domino kakel har också en lång historia av praktisk användning i trottoardesign och arrangemang av tatamigolv .
Själva problemet med det stympade schackbrädet föreslogs av filosofen Max Black i sin bok Critical Thinking (1946), med en antydan om den färgbaserade lösningen på dess omöjlighet. Den populariserades på 1950-talet genom senare diskussioner av Solomon W. Golomb (1954), George Gamow och Marvin Stern (1958), Claude Berge (1958) och Martin Gardner i hans Scientific American -kolumn " Matematical Games " (1957).
Användningen av det stympade schackbrädesproblemet i automatiserat resonemang härrör från ett förslag till användning av John McCarthy 1964. Det har också studerats inom kognitionsvetenskap som ett testfall för kreativ insikt, Blacks ursprungliga motivation för problemet. I matematikens filosofi har det undersökts i studier av matematiska beviss natur .
Lösning
Pusslet är omöjligt att slutföra. En domino som placeras på schackbrädet kommer alltid att täcka en vit ruta och en svart ruta. Därför kommer varje samling av dominobrickor som placeras på brädet att täcka lika många rutor av varje färg. Men två motsatta rutor har samma färg: båda svarta eller båda vita. Om de tas bort kommer det att finnas färre rutor av den färgen och fler av den andra färgen, vilket gör antalet rutor i varje färg ojämnt och brädet omöjligt att täcka. Samma idé visar att ingen dominobrickning kan existera när två rutor av samma färg (inte bara de motsatta hörnen) tas bort från schackbrädet.
Flera andra bevis på omöjlighet har också hittats. Ett bevis av Shmuel Winograd börjar med induktion. Om en rad har ett udda antal rutor som inte täcks av vertikala dominobrickor från den föregående raden, måste ett udda antal vertikala dominobrickor vid en given plattsättning av brädan sträcka sig in i nästa rad. Den första raden har trivialt ett udda antal rutor (nämligen 7) som inte täcks av dominobrickor från föregående rad. Således, genom induktion, rymmer vart och ett av de sju paren av på varandra följande rader ett udda antal vertikala dominobrickor, vilket ger ett udda totalt antal. Av samma resonemang måste det totala antalet horisontella dominobrickor också vara udda. Som summan av två udda tal måste det totala antalet dominobrickor – vertikala och horisontella – vara jämna. Men för att täcka det stympade schackbrädet behövs 31 dominobrickor, en udda siffra. En annan metod räknar kanterna på varje färg runt gränsen för det stympade schackbrädet. Deras siffror måste vara lika i vilken del som helst på schackbrädet, eftersom varje domino har tre kanter av varje färg, och varje inre kant mellan dominobrickor parar sig utanför gränserna för motsatta färger. Det stympade schackbrädet har dock fler kanter av en färg än den andra.
Om två rutor av motsatta färger tas bort, kan den återstående brädan alltid beläggas med dominobrickor; detta resultat är Gomorys teorem , efter matematikern Ralph E. Gomory , vars bevis publicerades 1973. Gomorys teorem kan bevisas med hjälp av en Hamiltonsk cykel av rutnätsgrafen som bildas av schackbrädesrutorna. Borttagandet av två motsatta färgade rutor delar upp denna cykel i två banor med ett jämnt antal rutor vardera. Båda dessa vägar är lätta att dela upp i dominobrickor genom att följa dem. Gomorys sats är specifik för borttagandet av endast en kvadrat av varje färg. Att ta bort ett större antal rutor, med lika många av varje färg, kan resultera i en region som inte har någon domino-beläggning, men för vilken färgbaserade omöjlighetsbevis inte fungerar.
Tillämpning på automatiserade resonemang
Domino sida vid sida problem på polyominoes , som stympade schackbrädeproblem, kan lösas i polynom tid , antingen genom att omvandla dem till problem i gruppteorin , eller som exempel på tvådelad matchning . I den senare formuleringen får man en tvådelad graf med en vertex för varje tillgänglig schackbräderuta och en kant för varje par intilliggande rutor; problemet är att hitta ett system av kanter som berör varje vertex exakt en gång. Liksom i det färgbaserade beviset på omöjligheten av problemet med det stympade schackbrädet, innebär det faktum att denna graf har fler hörn av en färg än den andra att den inte uppfyller de nödvändiga villkoren i Halls äktenskapsteorem, så ingen matchning existerar . Problemet kan också lösas genom att formulera det som ett problem med begränsningstillfredsställelse , och tillämpa semidefinitiv programmering på en relaxation .
År 1964 föreslog John McCarthy det stympade schackbrädet som ett svårt problem för automatiserade bevissystem , formulerade det i första ordningens logik och bad om ett system som automatiskt kan bestämma olösligheten av denna formulering. De flesta överväganden av detta problem ger lösningar "i begreppsmässig mening" som inte gäller McCarthys logiska formulering av problemet. Trots att det finns generella metoder som de som baseras på grafmatchning är det exponentiellt svårt för upplösning att lösa McCarthys logiska formulering av problemet, vilket lyfter fram behovet av metoder inom artificiell intelligens som automatiskt kan ändras till en mer lämplig problemrepresentation och för kunskap . representationssystem som kan hantera ekvivalenserna mellan olika representationer. Korta korrektur är möjliga med hjälp av upplösning med ytterligare variabler, eller i starkare bevissystem som tillåter uttryck av undvikbara kakelmönster som kan beskära sökutrymmet. Provassistenter på högre nivå kan hantera det färgbaserade omöjlighetsbeviset direkt; dessa inkluderar Isabelle , Mizar-systemet och Nqthm .
Relaterade problem
   |
Ett liknande problem frågar sig om en wazir som börjar vid en hörnruta på ett vanligt schackbräde kan besöka varje ruta exakt en gång och avsluta vid den motsatta hörnrutan. Wazir är en älvschackpjäs som bara kan flytta en ruta vertikalt eller horisontellt (inte diagonalt). Med liknande resonemang som det lemlästade schackbrädesproblemets klassiska lösning existerar inte denna wazirs turné. Till exempel, om den initiala rutan är vit, eftersom varje drag växlar mellan svarta och vita rutor, är den sista rutan i en komplett tur svart. Det motsatta hörnet är dock vitt. Denna typ av rundvandring på ett schackbräde utgör också grunden för en typ av pussel som kallas Numbrix , som ber om en rundtur där positionerna för vissa rutor matchar givna ledtrådar. Omöjligheten av en turné från hörn till hörn visar omöjligheten av ett Numbrix-pussel med ledtrådarna 1 i ett hörn och 64 i det motsatta hörnet.
De Bruijns sats handlar om omöjligheten att packa in vissa rätblock i en större kuboid. Till exempel är det omöjligt, enligt denna sats, att fylla en 6 × 6 × 6 ruta med 1 × 2 × 4 kuboider. Beviset använder ett liknande schackbrädesfärgningsargument som problemet med stympade schackbräde.
externa länkar
- Gomory's Theorem av Jay Warendorff, The Wolfram Demonstrations Project .