Ben's prikbord.

Een roofoverval

In januari 2007 schreef Gerard Vriens op de website van de AIgg het volgende artikel:

In de artificiële intelligentie wordt vaak gewerkt met zogenaamde "toy problems": simpele problemen, die geen praktisch nut hebben, maar wel uitstekend gebruikt kunnen worden om de mogelijkheden en beperkingen van bepaalde oplossingsmethoden te onderzoeken.

De volgende puzzel, overgenomen uit een bijdrage van Henk van Weers in het tijdschrift van de gebruikersgroep HCC!BASIC, is te beschouwen als een AI-probleem, omdat "logisch redeneren" doorgaans als een intelligente aktiviteit wordt beschouwd...

Programmeeruitdaging: "Wie heeft het gedaan?"
Naar aanleiding van een roofoverval heeft de politie 5 vemoedelijke daders gearresteerd, te weten: Appie, Bart, Chiel, Dirk en Evert. Probleem van deze arrestatie is, dat er ook één of meer onschuldigen bij kunnen zijn. Na weken van intensief speurwerk kwam vast te staan:

  1. Er is geen dader aan arrestatie ontkomen.
  2. Chiel kan dader zijn, alleen of samen met twee anderen, maar zeker niet met slechts één mededader.
  3. Als Appie schuldig is, is Evert onschuldig.
  4. Als Bart schuldig is, dan ook Chiel.
  5. Als Appie schuldig is of als Dirk schuldig is, dan is Chiel ook schuldig.
  6. Als Evert onschuldig is, is Bart dat ook.
  7. Als Dirk onschuldig is of Bart, dan is Evert ook onschuldig.
  8. Als Dirk onschuldig is, dan is Chiel dat ook.
  9. Als Appie onschuldig is, is Bart ook onschuldig.

Evenals de vorige keer gaat het hier niet om de oplossing zelf, maar om de oplossingsmethode. Hoe lossen intelligente wezens zoals mensen dit soort problemen op? (Volgens mijn "natuurlijke intelligentie" zijn Appie, Dirk en Chiel schuldig, Bart en Evert onschuldig.)

Kun je een programma bedenken, dat niet alleen dit specifieke probleem oplost, maar ook andere problemen van dit type? Voor dit probleem zijn er maar 25 mogelijkheden (elk van de vijf verdachten is hetzij schuldig, hetzij onschuldig) en 9 "feiten", dus het is nog mogelijk om alle combinaties te testen tegen alle feiten.
Maar wat als je een hele school met verdachten hebt? Of een heel voetbalstadion? Eén van de mogelijkheden is gebruik te maken van Prolog, een programmeertaal die speciaal is toegesneden op dit soort problemen en die veel wordt gebruikt in de Artificiële Intelligentie.
(GV 11 januari 2007)

Naar aanleiding van deze vraagstelling en nieuwsgierig geworden door de gesprekken hierover heb ik hieronder maar eens een poging gewaagd tot wat opheldering.Het resultaat volgt hier:

De puzzle:  1. Het begin.

Maart 2007.

Zoals Gerard schrijft is de puzzle op het eerste gezicht een typisch karweitje voor de computertaal Prolog. Even de regels in een prologprogamma opnemen en klaar ben je.Zo dacht ik in eerste instantie ook.Maar er zit een addertje onder het gras. De meeste voorwaarden beginnen namelijk op deze manier: Als iemand schuldig (onschuldig) is, dan ............

Het probleem schuilt in het feit dat je dat dus niet weet en juist moet uitzoeken! Bovendien kunnen er meer daders zijn. Daardoor vroeg ik me af: Welke groepssamenstellingen zijn er mogelijk  bij deze vijf vermoedelijke schuldigen?

In andere bewoordingen: welke deelverzamelingen zijn er van de verzameling ["Appie","Bart","Chiel","Dirk","Evert"] ?. Er blijken 31 echte deelverzamelingen mogelijk. En als je een verzameling ook als een deelverzameling van zichzelf beschouwt kom je op 32 mogelijke groepen van schuldigen. Bij elke groep van schuldigen zijn dan de onschuldigen uiteraard onmiddellijk bekend.
De aanpak in het programma is nu als volgt:

De combinatie die aan alle eisen voldoet levert het antwoord. Een dergelijke aanpak staat in de A.I. bekend als een "generate and test" methode. Daarbij worden dus alle mogelijkheden gegenereerd en vervolgens getest op juistheid. Dat is allemaal niet zo spectaculair. Maar omdat het een prolog programma is zien we het gebruik van feiten, regels, lijsten en recursie.Dat is weer eens wat anders.

Verder commentaar vind je in de broncode.

Je kunt de gratis personal edition van Visual Prolog, waarin het programma is geschreven, hieronder downloaden. Na downloaden en uitpakken van de logische puzzle kun je de projectfile inladen en het programma uitvoeren en bestuderen in een aangename programmeeromgeving. Wil je enkel en alleen de sourcecode even zien, download dan alleen de logische puzzle, pak de zipfile uit en lees "roofoverval.pro" met een editor naar keuze.

En nu gaan we maar nadenken over de vraag hoe zo'n puzzle moet worden opgelost wanneer de groepsgrootte veel groter is .........

De puzzle: 2.Voortschrijdend inzicht.

April 2007.

Er is nagedacht! Het grote bezwaar van het bovenstaande programma is natuurlijk dat alle combinaties eerst worden aangemaakt. dat is voor grotere programma's niet praktisch.

Het volgende programma genereert oplossingen met behulp van backtracking. Wanneer geen voorwaarden worden opgegeven produceert het programma alle mogelijke combinaties. Geef je de voorwaarden aan het eind op dan onstaat er net als in het bovenstaande programma een "generate and test"- situatie. Het is echter ook mogelijk om de checks eerder in de zoekboom uit te voeren. Zodra aan een voorwaarde niet wordt voldaan wordt er in de zoekboom gekapt. Het blijkt dat er drastisch in de mogelijkheden wordt gesnoeid. Ook puzzles van grotere omvang kunnen op die manier worden aangepakt.


class predicates
	schuldig : (boolean) multi (o).
clauses
	schuldig(true).
	schuldig(false).
clauses
	oplossing() :-
		schuldig(Appie),
		schuldig(Bart),
		if Appie = false() then Bart = false() end if,
		schuldig(Chiel),
		
		enz.

Om alles een beetje bij elkaar te houden, heb ik dit programma ook geplaatst bij het vorige. Voor de broncode moet je "backtracking.pro" bekijken. Mocht je die nog niet hebben moet je even de logische puzzle opnieuw downloaden.

De vraag is natuurlijk: kan het nog beter? Op de site van Visual Prolog staat een programma voor het oplossen van Sudoko-puzzles. Dat programma maakt voor de oplossingsmethode gebruik van "constraint satisfaction". Ik vraag me nu af of "constraint satisfaction" gebruikt kan worden voor ons probleem. Voor wie niet kan wachten om uit te vinden wat constraint satisfaction inhoudt zijn hier drie links:

Stevige kost. Dat staat vast.

De puzzle: 3. Op zoek naar de Heilige Graal.

Mei 2007.

In de AIgg-bibliotheek bevindt zich een boek: "Computational Intelligence". Hoofdstuk 4.7 is getiteld: "Constraint Satisfaction Problems". Daarin staat een voorbeeld aan de hand waarvan het begrip constraint satisfaction wordt duidelijk gemaakt. Gelukkig zijn de bijbehorende sheets hier te vinden:
Constraint Satisfaction Sheets. Als je door de sheets bladert kom je ook het voorbeeld tegen.

De schrijvers maken duidelijk dat een constraint satisfaction probleem het beste wordt gerepresenteerd door een netwerk. De knooppunten in het netwerk zijn de probleemvariabelen. De constraints liggen vast in de relaties tussen de variabelen, gerepresenteerd door de verbindingen in het netwerk. Een probleem wordt aangepakt via het doorzoeken van het netwerk. De zoek-strategieën die zij noemen zijn: generate_and_test, backtracking en consistency-algorithms.

Bij de consistency-algorithms heeft iedere variabele zijn eigen domein bij zich, dus alle waarden die een variabele kan aannemen zijn bekend. Het geheim zit hierin: het netwerk wordt doorzocht en waarden die niet voldoen aan een relatie worden uit het domein van een variabele verwijderd. De zoekruimte wordt tijdens het zoeken dus kleiner. Uiteindelijk moet het hele netwerk consistent zijn. Dat wil zeggen dat de overgebleven waarden aan de constraints voldoen en er dus een oplossing is. Daarbij geldt: Als er een domein leeg is, is er geen oplossing. Als elk domein precies één geldige waarde heeft is er een unieke oplossing. Als geen enkel domein leeg is en zijn minst één domein heeft meer geldige waarden dan kunnen er meer oplossingen zijn.

Deze consistency-algorithms zijn er in diverse soorten en smaken. Het meest toegepast wordt het AC-3 algoritme. Dat komt ruwweg gesproken hierop neer: de variabelen worden in een wachtrij geplaatst (queue). Dan wordt elke waarde uit het domein van een variabele vergeleken met elke waarde uit het domein van iedere buurman. Een buurman is daarbij elke variabele waarvoor een constraint geldt. Variabelen waarvan het domein wordt gereduceerd worden achter in de wachtrij geplaatst. Het zoeken gaat door tot de wachtrij leeg is.

De volgende output geeft misschien enig idee van de gang van zaken.


start queue ->["C","D","A","B","E"]
verwijder -> [] uit C (Nieuw) domein voor : C -> B [1,3,4] queue wordt -> ["D","A","B","E"]
verwijder -> [4] uit C(Nieuw) domein voor: C -> D [1,3] queue wordt ->["A","B","D","E"]
verwijder -> [1] uit C(Nieuw) domein voor C -> E [3] queue wordt -> ["A","B","D","E"]
verwijder -> [] uit A (Nieuw) domein voor A -> B [1,2,3,4] queue wordt -> ["B","D","E"]
verwijder -> [] uit A (Nieuw) domein voor A -> D [1,2,3,4] queue wordt -> ["B","D","E"]
verwijder -> [1] uit A (Nieuw) domein voor A -> E [2,3,4] queue wordt -> ["B","D","E"]
verwijder -> [] uit B (Nieuw) domein voor B -> A [1,2,4] queue wordt -> ["D","E"]
.........................................................................................
.........................................................................................
.........................................................................................
verwijder -> [] uit B (Nieuw) domein voor B -> E [2] queue wordt -> ["C","D"]
verwijder -> [] uit C (Nieuw) domein voor C -> B [3] queue wordt -> ["D"]
verwijder -> [] uit C (Nieuw) domein voor C -> D [3] queue wordt -> ["D"]
verwijder -> [] uit C (Nieuw) domein voor C -> E [3] queue wordt -> ["D"]
verwijder -> [] uit D (Nieuw) domein voor D -> A [4] queue wordt -> []
verwijder -> [] uit D (Nieuw) domein voor D -> B [4] queue wordt -> []
verwijder -> [] uit D (Nieuw) domein voor D -> C [4] queue wordt -> []
verwijder -> [] uit D (Nieuw) domein voor D -> E [4] queue wordt -> []
Resultaat:
domein: [1] van E
domein: [4] van A
domein: [2] van B
domein: [3] van C
domein: [4] van D

Integrated Development Environment voor dit programma

Het voorbeeld uit het boek en de sheets Example: Constraint Network heb ik gebruikt om een programma te schrijven dat het AC-3 algoritme hanteert. Een stevige klus mag ik wel zeggen. Je kunt het vinden in "ex_4_28.pro". Zonodig de logische puzzle opnieuw downloaden en je hebt hem binnen. Ook deze broncode heb ik van commentaar voorzien. Het voorbeeld Example: Scheduling Activities vind je in "ex_4_23.pro" met een "genereer en test" aanpak en in "ex_4_24.pro" staat een oplossing via backtracking.

Tenslotte: de vraag of dit AC-3 mechanisme gebruikt kan worden voor onze puzzle staat nog open. We houden de spanning er nog even in!

De puzzle: 4.Het einde van de zoektocht

November 2007

Geprobeerd om het probleem van de 5 rovers in het constraint satisfaction algoritme onder te brengen. Dat valt tegen!. De kern van het probleem zit in het feit dat de opgave bestaat uit als..dan_regels. Die zijn voor dit algoritme zeer omslachtig te formuleren. Bovendien verwijdert het algoritme zaken waarvan het zich niet kan herstellen omdat er geen backtracking in zit.

Wat nu? Door het voordurend omgaan met schuldige of onschuldige boeven begon ik me te realiseren dat het geheel verdacht veel te maken heeft met Boolse logica. De rakkers zijn wel of niet schuldig!. Als je het vanuit dat gezichtspunt bekijkt is het nog steeds een constraint satisfaction vraagstuk, maar dan wel boolean constraint satisfaction.

Hebben we misschien te maken met een SAT-probleem? SAT is de afkorting voor satisfiabilty ( = vervulbaarheid). Wanneer je een zin hebt in de taal van de propositielogica dan is de vraagstelling of die zin vervulbaar is, dat wil zeggen : is de formule waar? En zo ja: welke waarden voor de variabelen maken die zin waar?

Het SAT probleem is van groot belang in diverse gebieden van de computerwetenschappen zoals theoretische computerwetenschap , algoritmiek, kunstmatige intelligentie, hardware ontwerp, verificatie. Het probleem wordt een echt probleem als het aantal variabelen zeer groot wordt en men zoekt al jaren naar het beste algoritme. En daarmee zijn we op bekend terrein.

De eerste vraag is dus: kan ons probleem als SAT-probleem worden gezien? Daartoe moet onze roofoverval eerst in propositionele beweringen worden omgezet. Dat blijkt mee vallen.

Als Bart schuldig is,dan ook Chiel gaat bijvoorbeeld als volgt:

Bart -> Chiel

Als Appie schuldig is of als Dirk schuldig is, dan is Chiel ook schuldig, wordt:

(Appie # Dirk) -> Chiel

Soms is wat inventiviteit nodig.
Er is geen dader aan arrestatie ontkomen lees ik als: ze zijn niet allemaal onschuldig en dat wordt:

~(~Appie & ~Bart & ~Chiel & ~Dirk & ~Evert).

Zo kunnen alle beweringen worden geformuleerd. Ze worden tot één formule aanéén gesmeed en de vraag is voor welke waarden van de variabelen wordt deze formule waar?
De hele tekst staat hier.

De tekst kan in ons puzzleprogramma ( zonodig opnieuw downloaden) worden ingelezen via File/Open. Met Run/Waarheidstafel worden waarden toegekend aan de variabelen en wordt berekend of de formule waar is. Bij de 32 antwoorden blijkt de formule één keer waar te zijn.


..........
Appie = 1 Bart = 0 Chiel = 0 Dirk = 0 Evert = 0 Antwoord:0
Appie = 1 Bart = 0 Chiel = 0 Dirk = 0 Evert = 1 Antwoord:0
Appie = 1 Bart = 0 Chiel = 1 Dirk = 1 Evert = 0 Antwoord:1
Appie = 1 Bart = 0 Chiel = 1 Dirk = 1 Evert = 1 Antwoord:0
Appie = 1 Bart = 0 Chiel = 1 Dirk = 0 Evert = 0 Antwoord:0
.............

Het blijkt dus mogelijk om ons probleem als SAT-probleem te formuleren en via waarheidstabellen op te lossen. Waarheidstabellen zijn echter totaal ongeschikt om problemen met veel variabelen op te lossen vanwege het exponentieel gedrag dat zich in de zoekruimte voordoet.

De tweede vraag die dus beantwoord moet worden is nu: wat te doen bij een groot aantal variabelen? Vooral de laatste jaren zijn talloze zogenaamde SAT-Solvers ontwikkeld die dat probleem aanpakken. Er zijn zelfs wedstrijden aan de gang om te zien wie met de meeste variabelen het snelst een oplossing kan presenteren. Een algemeen overzicht met vele links is te vinden bij Wikipedia.

Deze programma's zijn vooral gebaseerd op de volgende algoritmen:

Beide algoritmen verwachten input in de vorm van een CNF-formule. Dat is een formule waarbij uitsluitend de connectieven of, en, niet gebruikt worden. Gelukkig is er een methode bekend die een formule in de taal van de propositielogica omzet naar CNF.

Tot slot:
Na het vinden van de oplossing via generate and test, backtracking en waarheidstabellen die alle gemakkelijk ons puzzeltje kunnen oplossen, blijkt dus dat we voor problemen met een groot aantal variabelen de oplossing moeten zoeken bij SAT-solvers. Hoe deze werken is een apart verhaal.