## Řešení problému SAT pomocí genetických algoritmů(SP, BP)

##### Zadání:

- název práce
Řešení SAT problému pomocí genetických algoritmů
Genetic SAT Solver
- katedra
Katedra počítačů
- obor
Výpočetní technika (bakalářský)
- studijní program
B
- vedoucí
Fišer Petr Ing.
http://cs.felk.cvut.cz/webis/people/fiserp.html
fiserp@fel.cvut.cz
- student
Hořejší Jaromír
horejj1@fel.cvut.cz
- pokyny
Vytvořte program řešící SAT problém pomocí genetických algoritmů. Porovnejte s ostatními dostupnými SAT solvery a zhodnoťte výsledky.

##### Aktuální stav projektu:

- Program randSat - Vytvoří booleovskou formuli podle zadaných parametrů pro testování v programu satGen
- Program satGen - SAT solver s využitím genetických algoritmůs (zdrojové kódy)
- Program, který byl použit k testování
- Solver Satzoo vč. naměřených výsledků
- Solver Walksat vč. naměřených výsledků
- Tabulky s výsledky testů, nalezení nejlepší kombinace selekce+křížení
- Tabulky s výsledky testů, posouzení vlivu velikosti turnaje na řešení
- Tabulky s výsledky testů, porovnání satGenu se solvery Walksat a Satzoo
- Seznam všech provedených testů s programem satGen vč. výsledků
- Titulní strana a abstrakt ve formátu .DOC
- Titulní strana a abstrakt ve formátu .PDF
- Závěrečná zpráva ve formátu .DOC
- Závěrečná zpráva ve formátu .PDF

##### Historie řešení projektu:

- 21.6. - doplněn vážený SAT, další úpravy dokumentace
- 11.5. - program umí pracovat nejen s 3-sat formulemi, ale i s n-sat
- 9.5.- 10.5. - turnaj, do kterého může vstupovat více jedinců, nová fitness maxOnes
- 21.4. - 8.5.2006 - dokončení dokumentace k projektu, vytvoření testovací verze programu, odstraněny další drobné chyby v programech
- 10.4. - 20.4.2006 - zpracování dokumentace k projektu
- 29.3. - 10.4.2006 - grafické a kozolové rozhraní plně funkční, přidán nový operátor křížení ve stylu GASAT Improvement
- 8.3. - 28.3.2006 - naprogramováno grafické rozhraní
- 6.3. - 7.3.2006 - navrhl jsem grafické rozhraní pro aplikaci
- 5.3. 2006 - trochu jsem rozšířil závěrečnou zprávu (asi o 10 stran)
- únor 2006 zlepšení programu satGen, vytvoření programu randSat, rozpracována závěrečná zpráva
- leden 2006 průběžná implementace vlastního systému satGen pro genetické algoritmy
- prosinec 2005 intenzivní studium problematiky genetických algoritmů
- říjen - listopad 2005 intenzivní studium problému SAT

##### Ukázky:

Obr. 1 - grafické rozhraní

##### Přepis korespondence mezi zadavatelem a řešitelem:

    ----- Original Message -----
    From: horejj1@fel.cvut.cz
    To: fiserp@fel.cvut.cz
    Sent: Tuesday, November 29, 2005 5:43 PM
    Subject: Dotaz - semestralni(bakalarska) prace

    Dobry den,
    na internetovych strankach VLSI mne zaujal projekt
    "Pou3ití genetických algoritmu v logické syntéze".
    Potreboval bych ale trochu vice podrobnosti, nez si tuto ulohu zavazne vyberu.
    Dival jsem se na internet a nejake materialy tykajici se genetickych algoritmu
    uz mam.
    Zajimalo by mne, co vsechno by mel zahrnovat semestralni projekt (zadany jsou 2
    ukoly - problem pokryti, splnitelnost formule)
    a jakym zpusobem lze dany projekt rozsirit na bakalarskou praci.

    Dekuji

    Jaromir Horejsi

    Dobry den,

    to tema muze byt velice siroke, uz na tom par lidi pracuje. Napr. problem pokryti je uz zabrany.
    Ale to nevadi, vzdycky se da neco vymyslet. Treba ten SAT problem by byl velice zajimavy
    (tim, ze by mozna vyzadoval nektere specialni techniky). Ale muzeme vymyslet i neco jineho.
    Jinak o co by slo:
    - naprogramovat v C++ nejaky ten algoritmus
    - muzete to bud naprogramovat cele sam, rucne, nebo s pomoci Galibu (viz Google)
    - pripadne to nejak zaclenit nekam (BOOM, PP)

    Muzeme se kdyztak nekdy sejit a prodiskutovat to. Viz muj "rezervacni system":

    http://cs.felk.cvut.cz/~fiserp/konzultace.html

    s pozdravem

    P.Fiser

    ----- Original Message -----
    From: "Jaromír Hořejší" yaaara@gmail.com
    To: "Petr Fišer" fiserp@fel.cvut.cz
    Sent: Thursday, December 01, 2005 5:57 PM
    Subject: Re: Dotaz - semestralni(bakalarska) prace

    Dobry den,
    tak ja bych si toto tema (Pouziti genetickych algoritmu v logicke
    synteze) vybral, pokud je stale jeste volne. Nejprve si zkusim promyslet
    mozny postup reseni problemu SAT (nejake studijni materialy jiz mam),
    pripadne bychom vymysleli jiny problem. Dam vcas vedet, ktery problem
    budu resit.

    Jaromir Horejsi

    OK. Dejte vedet.

    P.Fiser

    ----- Original Message -----
    From: "yaaara" yaaara@gmail.com
    To: "Petr Fišer" fiserp@fel.cvut.cz
    Sent: Thursday, January 05, 2006 4:54 PM
    Subject: Semestralni prace

    Dobry den.
    Asi pred mesicem jsem si zarezervoval tema semestralniho projektu
    (Pouziti genetickych algoritmu v logicke synteze). Mam v planu resit
    problem SAT. Neco malo jsem jiz vypracoval.

    Vzhledem k tomu, ze ted zacina zkouskove obdobi, bych se rad
    intenzivneji zacal problemem SAT zabyvat az po slozeni vsech zkousek.
    Vysledky sve prace hodlam predlozit v prubehu unora.

    Chtel jsem se timto mailem hlavne primomenout (protoze jsem se jiz
    dlouho neozval a ani jsme se nesesli), abyste na mne nezapomnel a
    nezadal toto tema napr. nakomu jinemu(na strankach VLSI je toto tema
    stale uvedeno jako volne).

    Jaromir Horejsi

    Dobry den,

    dobra. Beru to a pocitam s Vami. Ale stejne by nebylo od veci se sejit a dohodnout detaily. Co treba v utery ve 12:45?

    zdravi

    P.Fiser

    Dobre, tak v utery ve 12:45.
    J. H.

    OK. Zastavte se u me (306).

    P.F.

    Dobry den,

    zarezervoval jsem Vas na bakalarku. Prosim, napiste se na stranky projektu. Ja tam porad nemuzu zapisovat. Diky.

    https://service.felk.cvut.cz/prj/PROJECT19/

    A davejte tam vse, co mate.

    s pozdravem

    P.Fiser

    Uz jsem se tam zapsal. V nejblizsi dobe pridam odkazy na vysledky moji prace.

    Dobry den.

    Chtel bych se zeptat, jak bude probihat udeleni zapoctu ze semestralniho
    projektu.
    Ja delam dohromady SP a BP. To, co jsem dosud dokoncil, je k dispozici
    zde(http://yaaara2.czechian.net/sat/index.html).
    Zajimalo by mne, jestli to staci na udeleni zapoctu ze SP a jestli by bylo mozno
    zapsat zapocet zatim jenom do KOSu.
    S indexem bych si dosel pro zapocet az nekdy v prubeho prvniho vyukoveho tydne
    letniho semestru (posledni tyden zkouskoveho obdobi nebudu v Praze).
    Cela BP je zatim nedokoncena - mam v planu udelat rozsireni programu i
    doprovodneho textu na BP, takze celkovy rozsah a kvalita bude vetsi.

    Jaromir Horejsi

    Dobry den,

    zprava se mi zatim celkem libi. Detaily casem doladime.
    Trochu mi tam chybi nejake experimenty, pripadne srovnani s jinymi algoritmy. Ale to tedy vyresime v ramci bakalarky. Jeste se na ten program poradne podivam.
    Zapocet jsem Vam do KOSu napsal, takze se pak nejak ozvete, dohodneme se na dalsi strategii.

    s pozdravem

    P.Fiser

    Dobry den,

    doporucuji se podivat na stranku PAA (http://service.felk.cvut.cz/courses/36PAA/maxwsat.html), hlavne na ty odkazy, predevsim ten posledni (ppt). Najdete tam, jak delat tezke SATy.

    zdravi

    P.Fiser

    Quoting horejj1@fel.cvut.cz:

    > Zadam o konzultaci zitra dne 5.6. od 15:30.
    > Dekuji
    > Jaromir Horejsi

    Dobry den,

    omlouvam se, dneska tou dobou uz bohuzel nemuzu, narychlo jsem si uz neco
    naplanoval. Vyskytovat se budu nekdy pristi tyden, asi v pondeli. Pokud mate
    neco akutniho, napiste mail.

    zdravi

    P.Fiser

    Dobry den,
    nic akutniho nemam. Jen jsem se chtel zeptat, zda jste mou praci(SAT) jiz cetl a
    zda k ni mate nejake pripominky(abych mohl pripadne zacit vcas s opravami a
    nenechaval vsechno na posledni chvili).
    S pozdravem
    Jaromir Horejsi

    Dobry den,

    konecne jsem si to poradne prosel. Takze par poznamek jsem napsal primo do textu zlute.
    Jinak par globalnich veci:

    - nepouzivejte cislovani kapitol stylu 3.0. Je kapitola 3, pak podkapitola 3.1, atd.
    - radsi pouzivejte kurzivu pro promenne, v textu to cloveka mate.
    - nepouzivejte vyjadrovani se v mnoznem cisle (... popsali jsme). Psal jste to jen Vy.

    V kazdem pripade se mi to docela libi. Co ten vazeny SAT? Zkousel jste to? Byl bych moc rad, kdyby se to tam objevilo. Srovnat, jak dobre konverguje vazeny a nevazeny.
    Dale by se tam nekde mel objevit aspon jeden graf, ktery ukazuje, jak se vyviji populace behem generaci. Tj. aspon prumerna a max. fitness.

    Piste prosim zmeny pomoci revizi, at to pak nemusim vsechno cist znovu.

    A jen detail k uvodu:
    - abstract je cesky "anotace". A muzete to i trosku rezvest.

    Az tedy budete mit dalsi verzi, napiste mi, podivam se na to.

    zdravi

    Dobry den,
    provedl jsem doporucene zmeny a opravy.
    Napsal jsem to pomoci revizi. To, co jste oznacil zlute, jsem tam jeste nechal.
    Az to zkontrolujete, tak to odstranim.  Nove navrhy na opravu oznacte jinou
    barvou. Cisla tabulek a obrazku jsem zatim neopravoval.

    Vazeny SAT jsem zatim nedelal, doplnim pristi tyden.
    Aktualni text je na http://yaaara3.czechian.net/sat/SAT_v2.doc

    Jaromir Horejsi

    Dobry den,

    tak jsem si to konecte prosel, posilam zpet. Poznamky jsem napsal zelene. Uz je toho opravdu minimum.

    P.Fiser

##### vypracoval: Jaromír Hořejší
horejj1@fel.cvut.cz
(c) 2k5 - 2k6