Kategoriarkiv: Vetenskap

Vetenskapliga artiklar

Galileos hämd och den olycklige tidsoptimisten

En tidsoptimist är en person som ofta kommer för sent, genom att tro sig hinna mer än hen faktiskt gör. Jag tillhör den skara individer som identifierar sig som tidsoptimister och dagligen finner jag mig vara försenad till diverse program. Ifall jag själv inte påverkas av min försening, så finns det ofta någon annan som berörs. Det gynnar sig inte alltid att vara tidsoptimist i dagens hektiska samhälle där stora delar av människans vardag är tidsbestämd ner till sekunden.

Vi har idag klockor som är så exakta att GPS-satelliter måste med jämna mellanrum justeras, efter att märkbart påverkats av den relativistiska tidsdilatationen, så att de är i synk med de på jordytan. Tidmätningen har dock inte alltid varit lika exakt men den har alltid varit relevant. Redan de första människorna räknade dagar mellan regntider, mellan sommar och vinter. De bestämde tiden med hjälp av solen och en nedstucken käpp i marken. Deras klocka hade tre markeringar: soluppgång, middag och solnedgång. Deras dag hade två tidsangivelser: förmiddag och eftermiddag. De levde enkelt och kände knappast av någon tidspress. Detta var tidsoptimistens gyllene tidsålder.

Men sedan kom en vetenskapsman och förstörde allt. Antagligen visste han inte vad han hade upptäckt. Eller egentligen, kanske han inte visste just då. Men många år senare visste han precis vad upptäckten kunde användas till. Och han använde sig av den. På ett sofistikerat och mästerligt uttänkt sätt. Allt för att tala om för utvalda människor i kommande generationer att det var han som hade rätt. Utvalda människor därför att just de hade förmågan att inse varför och att de just därför kunde inse vad de skulle göra för att klara sig undan hans arv till eftervärlden, hans förbannelse, nedkallad över en i uppblåst övermod dömande mänsklighet, en mänsklighet som försökte göra något utanför dess förmåga.

Jag talar förstås om Galileo Galilei och hur han betraktade en ljuskrona som pendlade i vinddraget i katedralen i Pisa. Med sina egna hjärtslag som tidsbestämning insåg han att pendelns svängningstid, dess period, var oberoende av hur lång pendelrörelsen var. Han hade upptäckt det viktigaste elementet i ett urverk: tidhållaren, frekvensgivaren. I ett urverk ingår dessutom en kraftkälla, en regulator, en växelmekanism och en urtavla. Det hade förekommit klockor med mekaniska urverk innan Galileos upptäckt men de var närmast mekaniska leksaker.

Upptäckten av pendeln gjorde att dygnet kunde delas in på ett mycket mer exakt sätt än tidigare. Galileo var en vetenskapsman, fascinerad av astronomi, fysik och matematik. Han hade sedan tidigare förstått att människans förhållningssätt till ett nytt naturfenomen gick enligt en bestämd ordning: att förstå, att definiera, att behärska och sen att ta kontrollen över fenomenet och försöka styra över det.

Det här hade Galileo i bakhuvudet när han yttrade de berömda orden: ”och likväl rör den sig”. Det gjorde han efter att han tvingats att ta tillbaka påståendena om att jorden var rund och kretsade kring solen. Han dömdes till livstids husarrest. Kort innan sin död gjorde Galileo en ritning på ett pendelurverk. Han satte pendeln i svängning och bollen i rullning. Han visste att människan därefter inte skulle ge sig innan dagen var sönderspjälkad i minsta beståndsdel och tiden indelad i nanosekunder. Men han hade redan då insett att människan aldrig kommer att kunna styra över tiden.

Det här var hans hämnd. Ett arv som tog kål på den lycklige tidsoptimisten. Mänskligheten som ideligen försöker göra något utanför dess förmåga är för evigt dömd att känna stress och ideligen titta på klockan. Och konstatera att den likväl rör sig.

Sebastian Holm, evig tidsoptimist med konstant tidsbrist.

arm

Deus Ex Etik – vetenskap eller science fiction?

(OBS! Följande artikel innehåller bakgrundsinformation om spelen Deus Ex: Human Revolution och Deus Ex: Mankind Divided, publicerade av Eidos Montreal 2011 respektive 2016. Läs vidare med egen risk.)

Året är 2029. Förenta nationerna har framfört ett lagförslag med målet att återställa mänskligheten till dess naturliga tillstånd (Human Restoration Act). Lagen skulle medföra borttagning och förstöring av olagliga mekaniska proteser och förstärkningar. För att placera detta i sammanhang tar vi en kort genomgång av de senaste, knappa 100 åren [1].

1961 – MIT skapar den första datorstyrda robothanden.

1977 – Tai Yong Medical påbörjar produktionen av silikonbaserade proteser.

1978 – Forskare i Australien lyckas koppla ihop en elektronisk apparat med centrala nervsystemet på en fysiologisk nivå. Första cochleaimplantatet implementerades på en människa genom att använda denna teknologi.

1996 – Hugh Darrow återupptar och förnyar sin familjs protesföretag ett år efter att ha skadat sitt knä i en skidolycka och grundar därmed Darrow Industries.

1998 – Forskare vid Emory universitet skapar första hjärnimplantatet som kan styra rörelse.

2000 – Artificiell silikonretina (ASR) användes för första gången för att behandla individer med grova synfel.

2002 – Darrow Industries lyckas fläta samman elektroder med levande nervceller, för att skapa en omgivning där organisk cellvävnad kan acceptera syntetisk protesmaterial. Forskning inom ”mekaniska proteser och förstärkningar” ökar starkt inom Darrow Industries och Sarif Industries.

Bioniska ögat tillverkat av Sarif Industries.
Bioniska ögat tillverkat av Sarif Industries. Bildkälla: http://www.pcgamer.com/explore-deus-ex-human-revolutions-augmentations-with-sarif-industries-site/

2007 – Militärstyrkorna runt om i världen tillämpar mekaniska proteser i krigsföring, både på grund av styrka, men också för att värva skadade veteraner tillbaka till tjänst.

2013 – Den 50:nde sjukvårdskliniken för mekaniskt förstärkta patienter öppnas i New Delhi.

2020 – Mekaniska proteser och förstärkningar börjar bli vidsträckta. Darrow Deficiency Syndrome (DDS) diagnoseras i förstärkta individer. Den orsakar att kroppen förkastar proteserna och förstärkningarna på cellnivå. Ensamrätten till produktion av läkemedlet Neuropozyne säljs av Darrow Industries till företaget VersaLife.

2021 – Antoine Thisdale, en amerikansk arbetare i oljebranschen, stämmer staten för sin rätt att amputera sina armar för att få mekaniska armproteser. Högsta domstolen i USA bestämmer att Thisdale har rätten att amputera sina armar, och därmed lagstiftas den allmänna rätten för valfri förstärkning.

2022 – Mänsklighetens Front (Humanity Front), en politisk organisation emot mekanisk förstärkning grundas.

2024 – En amerikansk frågesportsdeltagare blir fast för att ha intelligenshöjande implantat, politiska rörelsen mot mekaniska förstärkningar ökar drastiskt i populäritet.

2027 – VersaLife klarar inte av att producera tillräckligt med Neuropozyne vilket skapar ett globalt underskott, speciellt hos de fattiga.

2027 – Den så kallade AUG-incidenten skapar världsomfattande kaos och ytterst negativa reaktioner mot mekaniska förstärkningar.

2028 – Förenta nationerna instiftar Taggart lagen som kräver klassifikation och uppföljning av alla mekaniska proteser och förstärkningar för att reglera industrin. Samlingen för de Förstärktas Rätter (Augmented Rights Coalition) grundas som en sammanbildning av grupperna runtom världen som stöder mekaniska förstärkningar.

Mänskligheten har alltid haft talang för propaganda.
Mänskligheten har alltid haft talang för propaganda. Bildkälla: http://www.pcgamer.com/deus-ex-mankind-divided-marketed-with-aug-awareness-posters/.

2028 – Som en följd av Taggart lagen blir mekaniska proteser och förstärkningar svårare och svårare att få tag på, vilket ökar efterfrågan på svarta marknaden. Mekaniska förstärkningar blir symboler för brottslighet och orenhet.

2029 –Förenta nationernas säkerhetsråd föreslår lagen Människans Återställning (Human Restoration Act) för att ta bort och förstöra olagliga förstärkningar. Debatten pågår…

Låt oss hoppa tillbaka till vår tid och värld. Berättelser och världar från TV-spel brukar vara fyllda med fantasifulla intriger och personligheter, men nu och då lyckas de säga något om den värld vi själva lever i. Världen i Deus Ex har en teknologidriven historia som täcker alla krav för ett gott och underhållande händelseförlopp inom science fiction. Om man bortser från årtalen så kan man dock inte undvika att dra paralleller till verkligheten.

Under de senaste 30 år har kolfiber, 3D-printning och biometri gjort det allt lättare att skapa förmånliga, välfunktionerande och individuella proteser för individer med amputerade lemmar. Implantat för retinan i ögat har utvecklats av företaget Second Sight för att lindra och upphäva symptom av vissa synsjukdomar [2]. Forskare vid Texas universitet skapade 2012 konstgjord muskelvävnad av nanotekniskt garn och paraffinvax, vilken kan generera 85 gånger mera ren mekanisk energi jämfört med t.ex. människans muskler [3]. Symbiosen mellan människa och maskin är definitivt inte lika fullständig som i världen av Deus Ex, men givet vetenskapens framgångstakt kan situationen uppenbara sig snabbare än vad man kunde tro.

Vilka frågor kommer mänskligheten att möta vid ett sådant tillfälle? Är vår moraletik utrustad till att behandla dessa frågor? I världen av Deus Ex svängde attityden snabbt från beundran och välmående till oförlitlighet och oro. Vad betyder det att vara människa? Är vi mera än summan av våra delar? Om våra kognitiva processer förbättras av ett implantat, är vi fortfarande i kontroll om hur vi tänker? Vem borde övervaka distributionen och användningen av mekaniska förstärkningar? Hur kontrolleras medicinering och reparation av sådana komplicerade konstruktioner? Hur undviker vi segregering och diskriminering?

Den senaste skandalen med priserna av EpiPen i USA visar att mänskligheten inte alltid lyckas göra bättre än sitt like i TV-spel. Neurologiforskaren Nadja Oertelt presenterade för en dryga månad sen en etisk ram inom vilken framtida beslut borde behandlas. Som avslutning följer hennes 8 riktlinjer för en etisk förstärkt framtid [4]:

  1. Utveckla rättvis politik och intelligent reglering av förstärkningsteknologier.
  2. Identifiera komplexiteten i mekanisk förstärkning och integrera komplexiteten med övervägandet av etiska beslut.
  3. Minimera social splittring och avbrott.
  4. Skapa undervisningsmaterial för allmänheten och för de som själva överväger förstärkning.
  5. Förstå rätterna och skyldigheterna av förstärkningssamhället
  6. Ta i bruk etiska principer för beteende och forskning.
  7. Stödja rättvisa och jämlikhet för alla.
  8. Garantera autonomi för individer i förstärkningsärenden.

 

  • Jonas

 

Källor

[1] Deus Ex-wikia,  Timeline, http://deusex.wikia.com/wiki/Timeline

[2] Second Sight, http://www.secondsight.com/

[3] University of Texas at Dallas, Wax-filled nanotech yarn behaves like powerful, super-strong muscle, ScienceDaily. ScienceDaily, 15 November 2012. <www.sciencedaily.com/releases/2012/11/121115141534.htm>.

[4] Nadja Oertelt, An ethical framework for human augmentation, Human by Design conference, August 3, 2016, http://www.humanxdesign.com/downloads/080116-HXD-EFHA-%C6%92.pdf

Algoritmisk Sudokulösning

Sudoku, eller “Number Place” som det ursprungligen hette är i dagens läge ett mycket välkänt logiskt pussel:

rank3Example rank3ExampleSolved

Givet ett 9 \times 9 rutfält delvis ifyllt av siffrorna 1-9 skall du fylla i resten av rutorna med siffrorna 1-9 så att varje siffra uppkommer endast en gång på varje rad/kolumn/liten ruta, vilka i exemplet omringas i bilden av de lite tjockare linjerna.

Sudoku pussel kan hittas överallt; många tidningar (t.ex. Hbl) publicerar sudokun dagligen, dessutom kryllar bokaffärerna av ”traditionella” och internet av elektroniska sudokun i varierande kvalitet. För de allra ivrigaste lösarna ordnas det årligen VM, med tusentals euron som pris. För den intresserade läsaren finns det i källorna ett par länkar om sudokuns historia, jag måste medge att jag hade trott att sudoku skulle härstamma från Japan, men den moderna varianten av sudoku skapades (högst troligen) av en 74-årig arkitekt från USA.

Det skulle kunna finnas ett antal olika aspekter att diskutera då det kommer till sudokun. Jag kommer att (igen) ta en datavetar-syn på det hela och undersöka till vilken grad datorer kan användas för sudokulösning. Det vill säga: hur svårt är lösning av sudokun för en dator och har människan någon chans klara sig mot dem? Mer specifikt så kommer jag att presentera tre olika algoritmer för sudokulösning samt jämföra dem med varandra.

Sudokulösning med datorhjälp

Näst går vi alltså igenom tre alternativa algoritmer för att lösa sudokun. För läsbarhetens skull kommer jag inte att gå in på detalj då det kommer till implementeringen av de mer komplicerade algoritmerna. Detaljerad förståelse för algoritmerna krävs inte i resten av texten och för de intresserade läsarna finns det en bilaga med (lite) mer detalj.

Algoritm 1:  SimpleSolver

Den första algoritmen vi undersöker är också den enklaste. Ifall jag skulle be 100 människor beskriva det simplaste sättet de kommer på för att lösa sudokun, skulle de flesta högst troligen beskriva SimpleSolver. Det handlar nämligen om att pröva alla de (ändligt många) sätten att fylla i de tomma rutorna. Algoritmen fungerar genom att gå igenom alla tomma rutor en åt gången och pröva alla möjliga siffror att sätta i dem. Efter att ha fyllt rutan granskar algoritmen att alla sudokuregler fortfarande uppfylls. Om allt är ok går algoritmen vidare till nästa tomma ruta, annars prövar algoritmen nästa siffra. Om algoritmen tvingas pröva alla siffror utan att kunna hitta en lösning går den tillbaka till föregående tomma ruta och prövar nästa siffra.

Med denna taktik kommer algoritmen i något skede att ha prövat alla möjligheter och därmed också hittat lösningen. SimpleSolver är väldigt simpel, implementation av den brukar vara en av räkneövningarna under grundprogrammeringskurserna i Gumtäkt.

Algoritm 2: DLXSudoku

Till skillnad från första algoritmen är de två andra algoritmerna för sudokulösning ursprungligen inte skapade för sudokun. Istället baserar de sig på idén att omvandla sudoku problemet till något annat (välkänt) problem och sedan lösa det andra problemet istället. Orsaken till att vilja göra såhär är att det ofta är lättare att omvandla problem än att lösa dem. Så om vi kan hitta andra problem som någon annan (lite fiffigare) människa har utvecklat effektiva lösningsalgoritmer för, kan vi dra nytta av dessa algoritmer genom att omvandla vårt problem. Detta är ofta tidseffektivare än att tillbringa en massa tid på att utveckla specialiserade algoritmer för just sudokun. Inom datavetenskap kallar man ofta denna process för en reduktion av ett problem till ett annat. Vår andra algoritm är baserad på en reduktion av sudokun till exact cover problemet och lösning av exact cover med hjälp av Algoritm X implementerad med dancing links: DLXSudoku.

Exact cover är ett ganska abstrakt problem: Givet en matris bestående av endast ettor och nollor är uppgiften att välja ut en delmängd av raderna i matrisen så att det bland de rader vi väljer ut finns exakt en etta i varje kolumn (Obs! Detta är inte den mest allmänna formuleringen av exact cover, men tillräcklig för vårt behov). Ett sudoku problem kan relativt enkelt omvandlas till en exact cover matris :

  • Varje tom ruta i sudokubrädet motsvaras av 9 rader i matrisen. Vi kallar dessa rader för Rr\#Cc\#1, \ldots, Rr\#Cc\#9 där den tomma rutan i fråga finns på rad r kolumn c.
  • Kolumnerna i matrisen representerar de olika sudoku reglerna:
    1. Varje ruta i sudokubrädet skall få exakt 1 siffra
    2. Varje kolumn på sudokubrädet skall bli ifylld av exakt en av varje siffra
    3. Varje rad i sudokubrädet skall skall bli ifylld av exakt en av varje siffra.
    4. Varje liten ruta skall bli ifylld av exakt en av varje siffra.

Alla av dessa regler representeras av kolumnerna så att kolumnen innehåller en etta på alla rader som uppfyller regeln (se exempel nedan).

Efter denna konstruktion kan vi lösa exakt cover problemet och omvandla lösningen till en lösning av sudokut helt enkelt genom att fylla i sudokut enligt de rader Rr#Cc#x som vi valt ut till exact cover lösningen. Notera specifikt att kolumnerna i exact cover matrisen som representerar kravet ”varje ruta på sudokubrädet får exakt ett värde” försäkrar oss om att exact cover lösningen innehåller för varje rad r och kolumn c på sudoku brädet, exakt en rad Rr#Cc#i från exact cover matrisen. För den intresserade läsaren finns det som bilaga till denna text en beskrivning på hur DLX fungerar. Här nöjer vi oss med att nämna att algoritmen har populariserats av Donald Knuth, som även har utvecklat det (inom naturvetenskaper) mycket använda LateX typsättningssystemet.

rank2Exampel

Exempel: Vi reducerar 4 \times 4  sudokut ovanför till exact cover. För detta sudoku får vi en exact cover matris med 8 (antalet tomma rutor) \times 4 rader. Bilden nedan visar en del av den:

ExactCover I bilden representerar första kolumnen kravet: ”Rutan på rad 2 kolumn 1 måste få exakt 1 värde”. Vi ser att kolumnen innehåller en etta på varje rad vars val fyller i rutan och 0 annars. Andra kolumnen representerar kravet ”Någon ruta på rad två måste innehålla en etta”, tredje kolumnen representerar: ”Första kolumnen måste innehålla en fyra” och fjärde ”lilla rutan uppe till höger måste innehålla en etta”, vi märker specifikt att fjärde kolumnen innehåller en etta endast på första raden. Detta betyder att vi måste välja första raden till exact cover lösningen vilket i sin tur betyder att rutan i kolumn 1 rad 2 kommer att innehålla en etta.

Algoritm 3: SATSudoku

Den sista av våra algoritmer reducerar sudoku till det kanske mest kända ”svåra” problemet inom datavetenskap, nämligen satisfiability (SAT). För att kunna beskriva SAT måste vi påminna oss om logik kursen i gymnasiet och specifikt de delarna som handlade om propositionslogik.

Propositionslogik är ett väldigt enkelt logiskt ”språk” där man formar formler genom att binda ihop sanningsvariabler (dvs. variabler som antingen kan vara sanna eller falska) med hjälp av \land (OCH), \lor  (ELLER) och \neg (INTE). (Obs. det finns ett antal olika sätt att definiera propositionslogik, vi använder det simplaste möjliga som räcker för vårt behov). Givet en propositionslogisk formel går SAT problemet ut på att hitta ett sätt att ge sanningsvärden (sant eller falskt) åt variablerna som gör att hela formeln blir sann. Sanningsvärdet för en formel definieras utgående från sanningsvärden för de delformler den innehåller:

  • Om formeln endast består av en enda variabel är dess sanningsvärde lika med sanningsvärdet för variabeln.
  • Sanningsvärdet för \lnot A är motsatsen till sanningsvärdet för formeln A
  • Formeln A \land B är sann ifall både formlerna A och B är sanna
  • Formeln A \lor B är sann ifall antingen A eller B (eller båda) är sanna.

Då vi i denna text pratar om att lösa SAT menar vi att hitta ett sätt att ge värden åt variablerna i en given formel så att formeln blir sann. Vi kallar detta sättet för en ”lösning” av SAT. (Notera att detta inte är en allmän definition av SAT problemet, men tillräcklig för oss.)

SAT är ett mycket välkänt problem inom datavetenskap. I dagens läge existerar det effektiva algoritmer för att lösa formler som består av hundratusentals variabler och miljontals delformler. För att kunna använda dessa algoritmer för att lösa sudokun måste vi från ett givet sudokubräde kunna forma en propositionsformel som tillåter oss omvandla en lösning på SAT problemet till en lösning på sudoku problemet.

För varje ruta, säg på rad r kolumn c, introducerar vi 9 sanningsvariabler: v^{rc}_1, \ldots, v^{rc}_9. Meningen med dessa variabler är: ”v^{rc}_k är sann om och endast om rutan på rad r kolumn c får värdet k i sudokulösningen”. Vår formel kommer att bestå av 5 olika delformler, fyra olika beskrivningar på de olika sudokureglerna och en som beskriver de siffror som är färdigt ifyllda:

1) Varje ruta skall få exakt ett värde. För en fixerad ruta på rad r kolumn c beskrivs detta krav av en logisk representation av: \sum_{j=1}^9 v^{rc}_j = 1. Det finns olika sätt att representera detta som propositionslogik. Ett av de simplaste är att använda formeln: v^{rc}_1 \lor v^{rc}_2 \lor ldots \lor v^{rc}_9 för att se till att rutan får minst ett värde och 27 formler av formen: \lnot (v^{rc}_i \land v^{rc}_j) \quad \forall i < j för att se till att den får högst ett värde. I vår implementation använder vi oss av ett lite annorlunda sätt att representera samma sak (kallas för sequential counter). För den intresserade läsaren finns det referenser.

2) Varje rad skall få en av varje värde. För en fixerad rad R beskrivs detta av (del)formeln:

\bigwedge_{k=1}^9 \left(\sum_{c=1}^9 v^{Rc}_k = 1\right)

som omvandlas till propositionslogik precis som i punkt 1.

3) Varje kolumn skall få en av varje värde. För en fixerad column C beskrivs detta av formeln:

\bigwedge_{k=1}^9 \left( \sum_{r=1}^9 v^{rC}_k = 1 \right)

4) Varje liten ruta skall få en av varje värde. För t.ex. lilla rutan längst upp till vänster beskrivs detta av formeln:

\bigwedge_{k=1}^9 (v^{11}_k + v^{12}_k + v^{13}_k + v^{21}_k + v^{22}_k+v^{23}_k+v^{31}_k+v^{32}_k+v^{33}_k = 1)

5) Varje redan färdigt ifylld ruta motsvaras av en formel som tvingar motsvarande variabel att sättas till sant. Så ifall rutan på rad r kolumn c har färdigt ifyllt värdet k lägger vi med delformeln v^{rc}_k till hela formeln.

Vår sista algoritm för sudokulösning bygger upp ett SAT problem såhär och ger den åt en SAT algoritm. Så länge ursprungliga sudokut har en lösning kommer SAT algoritmen att hitta en lösning på SAT problemet. Sedan omvandlas  SAT lösningen till en sudoku lösning: rutan på rad r kolum c i sudokubrädet fylls i med det värde k för vilket variabeln v^{rc}_k är sann i SAT lösningen. Delformeln vi satt med i punkt 1 här ovan försäkrar oss om att det finns exakt en sådan för varje tom ruta.

rank2Exampel

Exempel: Vi fortsätter med samma exempel som tidigare. Fullständiga propositionsformeln som beskriver detta exempel är för lång för att skrivas ner för hand. Men här följer en del illustrerande exempel   

  1. Rutan på rad 2 kolumn 1 skall få exakt ett värde: (v^{21}_1 \lor v^{21}_2 \lor v^{21}_3 \lor v^{21}_4) \land \lnot (v^{21}_1 \land v^{21}_2) \land \lnot (v^{21}_1 \land v^{21}_3) \land \lnot (v^{21}_1 \land v^{21}_4) \land \lnot (v^{21}_2 \land v^{21}_3) \land \lnot (v^{21}_2 \land v^{21}_4) \land \lnot (v^{21}_3 \land v^{21}_4).
  2.  Kolumn 1 måste innehålla en etta: (v^{11}_1 \lor v^{21}_1 \lor v^{31}_1 \lor v^{41}_1) \land \lnot (v^{11}_1 \land v^{21}_1) \land \lnot (v^{11}_1 \land v^{31}_1) \land \lnot (v^{11}_1 \land v^{41}_1) \land \lnot (v^{21}_1 \land v^{31}_1) \land \lnot (v^{21}_1 \land v^{41}_1) \land \lnot (v^{31}_1 \land v^{41}_1).
  3. Rad 1 måste innehålla en två: (v^{11}_2 \lor v^{12}_2 \lor v^{13}_2 \lor v^{14}_2) \land \lnot (v^{11}_2 \land v^{12}_2) \land \lnot (v^{11}_2 \land v^{13}_2) \land \lnot (v^{11}_2 \land v^{14}_2) \land \lnot (v^{12}_2 \land v^{13}_2) \land \lnot (v^{12}_2 \land v^{14}_2) \land \lnot (v^{13}_2 \land v^{14}_2).
  4. Vissa rutor är färdigt ifyllda: v^{11}_3 \land v^{12}_4 \land v^{13}_1 \land v^{22}_2 \land v^{33}_2 \land v^{42}_1 \land v^{43}_4 \land v^{44}_3.

Bilagan till denna artikel går in på (lite mer) detalj om hur en SAT algoritm oftast fungerar.

Vilken är bäst?

Nu är det dags för den mest intressanta frågan; vilken är bäst? För att kunna testa detta fick jag hjälp av Toffe som implementera SimpleSolvern och Lasse som implementera DLXSudoku. Själv implementerade jag SATSudoku. Tack till både Toffe och Lasse!

Innan vi går till resultaten vill jag påpeka att skillnaderna vi kommer att se i dessa algoritmer inte beror på implementationerna, resultaten kan inte och skall inte användas för att jämföra våra kodningskunskaper.

Jag valde på måfå ut 3 sudokun av storlek 9 \times 9 och tog tid på hur länge var och en av våra algoritmer tog på sig för att lösa dem. Resultaten finns nedan:

SudokuEasy

Det var ju lite tråkigt inte sant? Till och med den simplaste algoritmen löser alla 3 på under 1.5s, de mer avancerade lösarna tar under en tiondels sekund på sig. Detta illustrerar orsaken till varför jag bara hade tre sudokun; faktum är att de allra flesta normala sudokun är så gott som triviala för en dator. Det går att designa problem som vår SimpleSudoku inte skulle kunna lösa, men redan genom att ha SimpleSudoku  pröva siffror i slumpmässig ordning istället för storleksordning så klarar även den av så gott som alla 9 \times 9 sudokun snabbare än vad det skulle ta för människan att skriva ner en färdig lösning. Så det ser inte så hemskt lovande ut för oss människor.

Det verkar alltså klart att om man behöver få många sudokun löst snabbt är det mer tidseffektivt att koda en lösare än att lösa dem själv. Dock kan man efter dessa resultat  fråga sig varför man över huvudtaget borde sätta ner tid på att implementera något som helst mer avancerat än SimpleSudoku?

Ifall man bara är intresserad av 9 \times 9 sudokun är svaret: man borde inte. Men, om vi tillåter större sudokun blir saker och ting intressantare. Forskningsresultat inom sudokulösning (ja, det finns sådana) pratar ofta om ordningen (rank) av ett sudoku. En normal sudoku är av ordning 3 och allmänt så skall en sudoku av ordning n lösas på ett n^2 \times n^2 bräde. Så en 4 \times 4 sudoku är av ordning 2 och en 16 \times 16 sudoku är av ordning 4. Alla av våra algoritmer kan användas för att lösa sudokun av vilken ordning som helst. Dessutom borde större sudokun vara bättre för att jämföra algoritmer, intuitivt känns det ju ganska klart att ett större sudoku borde vara svårare än ett mindre.

SudokuHard

Resultaten finns ovan och nu börjar vi på riktigt märka skillnader i algoritmerna. SimpleSolvern klarade inte av en enda av dessa problem på under en timme (gränsen på lösningstiden). Däremot klarar sig både SATSudoku och DLXSudoku ganska väl, speciellt på ”enkla” sudokun. Av dessa två klarar sig SATSudoku lite bättre än DLX: den klarar av en ordning större ”lätt” problem och en ordning större ”svårt” problem.

Vad lär vi oss av detta? Jo, om du bara vill lösa ett enda normal stort sudoku är det fiffigare att ta papper och penna än börja koda. Skall du lösa 1000 normala sudokun kan du be datorn göra det på det enklaste möjliga sättet. Skall du lösa ett enkelt 15^2 = 225 \times 225 sudoku, så går det också att fixas, dock med lite mer möda. Men om du vill lösa ett svårt 49 \times 49 sudoku? Då är det dags att ta fram pennan igen, skriva ett stort ”LÖS SJÄLV” på hela brädet, och ta en öl istället.

Slutligen vill jag lämna er med det största sudokut som våra algoritmer klarade av och det minsta som de inte klarade. Om någon av er får någondera löst kan ni lämna en kommentar så sätter jag med er i resultaten.

Jeremias

BILAGA:

Algorithm X, Conflict Driven Clause Learning and Dancing Links for Sudokusolving.

Källor:

Ballmer Peak – Kan XKCD ha rätt?

Ballmer  Peak är ett relativt känt begrepp bland folk som har läst några kurser data, samt vem som helst som känner sådana dataloger som inte förstår att hålla sina skämt till sig själva. Ursprunget till begreppet kan ni hitta i er sångbok på sidan 60, på samma sida som det i min sångbok finns en god jul hälsning samt ordet ”dubbelsup”.

ballmer_peak

Det handlar alltså om påståendet att det skulle finnas någon koncentration av alkohol i blodomloppet som betydligt skulle öka programeringsförmågan. XKCD påstår att koncentrationen skulle ligga någonstans mellan 1.29 och 1.38 promille, vilket motsvarar ca 7 portioner på 2 timmar för någon som väger 70 kg. Kan det alltså vara möjligt att det lönar sig dricka 7 öl innan man börjar med sina data räkneövningar? Detta låter ju som något värt att undersökas.

Då man designar ett experiment för att testa något sånt här möter man genast på en massa svårigheter. Begreppet ”programming ability” som finns på y-axeln i serien är inte speciellt formellt. Det är inte heller enkelt att få tag på bra samt billiga mätare för att mäta alkoholhalt i blodet. Vidare existerar det ett antal andra variabler som är svåra att kontrollera. Om man ger sju öl åt någon som just och just kan ”Hello World” i java så är det inte hemskt överraskande att den inte får något mer än Hello World gjort efter att ha druckit dem heller. Man kan alltså förvänta sig att resultaten varierar mycket från person till person beroende på dens tidigare programmeringsförmåga. Vi skulle alltså behöva en stor mängd människor att testa med.

IMG_1017

Då man översätter stor mängd till Spektrum språk får man 5. En onsdagskväll for vi alltså mot Klubben med 5 ivriga kodare för att se ifall det ligger något bakom det hela. Som uppgifter hade jag valt räkneövningar från årets Tietorakenteet ja Algoritmit kurs (TiRA). TiRA brukar man gå under sin första vårtermin som datalog, dvs. efter ett halvt år av studier. En stor del av deltagarna på kursen tycker om TiRA så mycket att de går den flera år i rad.

En viktig detalj om TiRA uppgifter är att det ofta krävs lite mer än ren programmeringsförmåga för att lösa dem. Man måste tänka på detaljer som hur effektiv koden är. Ett exempel på en lite lättare uppgift som var med i vårt test var att koda en metod som kollar ifall två givna ord är anagram av varandra.  För den intresserade läsaren finns det i källorna en artikel som behandlar exempel på kod effektivitet via fibonacci talens uträckning (som också var en av uppgifterna). Jag vill tacka TiRA handledarna och föreläsaren för uppgifterna och testen till uppgifterna.

Efter att alla blåst nollor satt vi igång. Jag hade förberett 6 ronder med 4 uppgifter per rond. Efter första ronden blev det klart att detta var allt för mycket. Det var nämligen endast en av testpersonerna som fick två uppgifter gjorda på tiden 20.14. För resten av ronderna mätte vi därför tid taget per uppgift med en timeout på 20 minuter per rond. Mellan varje rond dracks det uppfriskningar och hölls en paus på 15 minuter.

IMG_1021

NimetönUppgifter

Resultaten hittas i graferna. Stapeldiagrammet till höger visar mängden lösta uppgifter varje runda, andra grafen visar mätta promillehalten innan varje runda. I äkta statistik anda borde jag nu hitta på metriker vilka skulle få resultaten att bli imponerande. Men först vill jag kommentera på en observation jag gjorde under ronderna. Som ni ser så steg promill nivåerna inte hur högt som helst. Dock skulle man på ljudnivån som testgruppen höll inte ha trott att de flesta var i körskick de första tre ronderna. En placebo-effekt kunde alltså definitivt märkas, inte så mycket på själva problemlösningen som allmänna beteendet.

När det kommer till de egentliga resultaten krävs det mycket fantasi för att kunna säga något. Det enda jag kommer på är att under första rundan (efter en enda öl) löste hela gruppen flest uppgifter, vilket med lite handviftande skulle kunna tyda på att en öl lugnade ner testgruppen tillräkligt för att öka totala mängden uppgifter löst. Men som sagt, mycket handviftande krävs för att dra några statistiskt signifikanta slutsatser.

IMG_1030

Därför är det säkert bäst att spela beer pong istället.

IMG_1033

Det blev alltså inte så mycket bevisat den kvällen. Tur i oturen så har effekten av alkohol på människokroppen och tankeverksamheten undersökts i bredare skala annanstans. De forskningar som jag hittat undersöker oftast kopplingen mellan kreativt tänkande och alkoholkonsumption. Kreativt tänkande är mycket viktigt i problemlösning och kodning, så eventuella resultat borde gå att applicera på Ballmer Peak också.

Alkohol gör en människa full, detta torde de flesta av er veta. Men en liten mängd alkohol kan i vissa fall förbättra prestandan. Ett exempel av detta är sporter som kräver lugnhet och stadig hand, så som skytte. Dock måste det ju påpekas att det finns många orsaker  varför det ändå inte skulle vara en bra idé att ha deltagare dricka alkohol innan de far ut till banan och siktar skjutvapnen mot små tavlor.

När det kommer till kopplingen mellan alkohol och kreativitet så finns det en del resultat som tyder på att en promillehalt på 1.2 -1.4 förbättrar vissa aspekter av kreativt tänkande men försämrar andra. Specifikt så lär lite alkohol göra hjärnan bättre på att kombinera information som den har fått för att skapa lösningar; ni vet de där ”ahaa” upplevelserna som kommer då man minst förväntar sig. Däremot gör alkohol hjärnan sämre på att ta in ny information samt verifiera att lösningarna den hittar på är korrekta. Det har även gjorts undersökningar om effekten av alkohol på kreativ produktivitet bland 34 kända författare, kompositörer samt andra artister under 1900-talet. Resultatet var ofullständiga och delvis motsägelsefulla. I 75% av fallen hade alkohol en negativ inverkan på produktiviteten, speciellt en långvarig alkoholanvändning. En direkt positiv inverkan kunde observeras i 9% och en indirekt i 50%. I undersökningen hittades också tecken på att kreativ produktivitet även ökar alkoholintagningen, vilket gör det hela till ett ”hönan och ägget” problem. Dock rapporteras inte mängder alkohol kvantitativt, vilket gör undersökningen svårare att applicera på Ballmer Peak.

En del undersökningar stöder tanken om att alkohol egentligen fungerar som placebo när det kommer till kreativitet och problemlösning. I en undersökning drack olika testgrupper olika starka vodka tonics utan att veta exakt hur starka var och en fick. En positiv effekt av alkohol för problemlösning kunde observeras i alla testgrupper, vilket föreslår att effekten kan bero på att man förväntar sig bli bättre om man dricker lite.  Liknande resultat märktes bland våra testpersoner; att man förväntar sig vara onykter bidrar också en hel del till hur onyktert man beter sig.

Avslutningsvis tänkte jag visa er en alternativ tolkning av balmers peaken. XKCD har tydligen endast valt att använda projektionen av den egentliga 3D kurvan till två dimensioner. Nästa gång röstar jag för att vi kör liknande tester i Mallbolage istället med endast ”Hello world” som uppgift. Tack till alla frivilla som hjälpte till med testandet, hoppas ni hade lika roligt som jag.

Ballmer

Jeremias

P.S. Mallbolage lär vara världens svåraste kodspråk.

Källor:

http://www.laskurit.fi/promille/?amount=10&sex=f&weight=70&hours=2&submit=Laske+promillem%C3%A4%C3%A4r%C3%A4

https://www.ics.uci.edu/~eppstein/161/960109.html

https://xkcd.com/323/

http://www.scriptol.com/programming/hello-world.php

http://onlinelibrary.wiley.com/doi/10.1002/j.2162-6057.1999.tb01036.x/abstract

http://onlinelibrary.wiley.com/doi/10.1111/j.1360-0443.1990.tb03726.x/abstr

http://www.jstor.org/discover/10.2307/1423036?uid=3737976&uid=2&uid=4&sid=21103808186867

http://www.usada.org/prohibited-list/athlete-guide/

http://www.healthcentre.org.uk/sports-medicine/sports-alcohol-sports-performance.html

http://www.sultanik.com/Blog%3aBallmer

Spektrums hedersmedlemmar (del 2 av 2)

Nu har det gått en vecka sedan två av Spektrums hedersmedlemmar presenterades och nu är det dags för de resterande tre. I dagens presentation kommer två kemister och en datalog att presenteras. Ordningen kommer att vara från den minst kända till den mest kända, om man ser på antalet publikationerna i Web of Knowledge.[1] Därför börjar vi med Linus Torvalds, som dock med minst publikationer säkert är den mest kända (åtminstone på ett allmänt plan). Efter det kemisterna doc. Henrik Konschin och professor emeritus Pekka Pyykkö.

Linus Torvalds

torvalds

Linus Torvalds började studera datavetenskap vid Helsingfors universitet år 1988 direkt efter gymnasiet. Efter ett år av studier tjänstgjorde han vid Nylands brigad. Under de kommande åren började han utveckla Minix, ett unix-liknande operativsystem. På grund av att han inte var helt nöjd med terminalemulatorn i Minix så skrev han en egen. Det här blev sedan grunden för Linux.[2] Även under denna tid var han en aktiv medlem i Spektrum (Det är väl bara att fråga de personer som var aktiva under samma tid).

Den 17 september 1991 utkom version 0.01 av Linux (och en månad senare version 0.02). I mars 1994 utkom Linux 1.0 på datalogen vid Helsingfors universitet, då med ett grafiskt användargränssnitt. År 1996 slutförde han sin pro gradu-avhandling med namnet ”Linux, a portable operating system” och fick ett laudatur för sitt arbete. Han flyttade sedan till USA och började jobba på Transmeta, som designade elsnåla processorer. År 2003 sade han upp sig och började på heltid att jobba med Linux-kärnan för Open Source Developement Labs. Detta företag slogs sedan ihop med ett annat och heter numera Linux Foundation.[2]

Ett annat program som Torvalds har kodat är Git.[3] Git är ett version-kontroll program (eng. version control), som håller reda på olika versioner av ett program. Programmet var i början designat för att hålla reda på Linux-kärnan men är nuförtiden en av de mest använda version-kontroll programmen. Torvalds blev år 1999 hedersdoktor vid Stockholms universitet[4] och hedersdoktor vid Helsingfors universitet år 2000.[5]

Doc. Henrik Konschin

Henrik Konschin är den person av dessa tre som det är absolut svårast att hitta någon information om. Han har åtminstone blivit medlem i Spektrum år 1968 och varit hjälpande KM det året. I början av sin akademiska karriär har han gett ut en massa artiklar om spektroskopi och Ramanspektroskopi.[1] År 1985 fick Konschin sin doktorstitel i kemi, med en doktorsavhandling om Ramanspektroskopi och kvantkemiska beräkningar för hydroxi- och metoxisubstituerade bensener.[6] Efteråt har han även gett ut artiklar om både Ramanspektroskopi och kvantkemiska beräkningar för diverse material och ämnen.[1] Han har jobbat på svenska kemen som föreläsare och gett ut några (delar av) böcker, t.ex. en om spektroskopi[6] och en med räkneuppgifter till fysikalisk kemi.[7] Henrik Konschin är även mycket känd inom Spektrum, inte bara för att han varit föreläsare, utan för stipendiet HK:s gunstling.

Professor emeritus Pekka Pyykkö

pyykko

Pekka Pyykkö blev magister år 1964, nästa år licentiat och år 1967 doktor från Turun Yliopisto. Under de nästa 7 åren var han utomlands på diverse ställen runtom i europa. Efter det jobbade han 10 år som ”Associate professor” (vet inte exakta svenska översättningen) vid Åbo Akademi, med inriktningen kvantkemi. År 1984 blev han professor i kemi vid Helsingfors universitet och fr.o.m 1995 forskningsprofessor. Emeritus titeln fick han år 2009.[8]

Pyykkö har hittills gett ut över 300 artiklar och även tre stycken böcker (inget konstigt att han toppade listan på web of Knowledge av dessa tre).[1] De tre böckerna han har skrivit är ”Relativistic Theory of Atoms and Molecules I – III”. Dessa tre böcker behandlar som namnen säger den relativistiska teorin för atomer och molekyler och är samlingar om vad man vet om fenomenet. Böckerna är skrivna under tre olika decennier och sammanfattar det nya som har hänt mellan dem. Ett av hans nyare papper, som verkar mycket intressant, är ett expanderat periodiskt system.[9] I den här artikeln beskrivs ordningen hur elektronskalen fylls, m.h.a. datorsimuleringar, för atomer med upp till 172 elektroner.

Fredi

[1] Web of Knowledge, http://apps.webofknowledge.com/
[2] Torvalds & Diamond, Just for fun. Menestystarina / The Story of an Accidental Revolutionary
[3] Git Homepage: git-scm.com
[4] www.su.se/om-oss/priser-utmarkelser/hedersdoktorer
[5] www.helsinki.fi/promootiot/filtdk/text6.htm
[6] www.finna.fi
[7] HELKA, Helsingin Yliopiston kirjastot: helka.linneanet.fi
[8] Pekka Pyykkös CV: www.chem.helsinki.fi/~pyykko/curriculum/curriculum.html
[9] Pekka Pyykkö, Phys. Chem. Chem. Phys.,2011,3, 161-168

Bilden på Pyykkö: http://www.chem.helsinki.fi/~pyykko/
Bilden på Torvalds: http://sv.wikipedia.org/wiki/Linus_Torvalds