% \date{15. května 2007}
% \setyear{2007}
% \author{Kamil Dudka}
% \title{Knihovna pro~práci s~objekty ve~sdílené~paměti}
% \FITproject{BP}
\chapter{Úvod}
Úkolem bylo vytvořit program, který řeší problém \textit{splnitelnosti množiny výrokových pro\-měnných} pomocí \textit{genetického algoritmu}.
Problém splnitelnosti množiny výrokových proměnných je znám v literatuře jako \textit{SAT Problém}\footnote{Název je převzatý z angličtiny -- SATisfiability problem.}. Jedná se o takzvaný \textit{rozhodovací problém}, jeho přesnou definici je možné nalézt v~\cite{TIN}. Rozhodovací problém je zadán množinou formulí výrokové logiky. Úkolem je rozhodnout, jestli existuje takové ohodnocení výrokových proměnných, pro které jsou všechny formule splněné.
Algoritmus, který tento problém rozhoduje, spadá do třídy složitosti \textit{NP}. Přesnou definici této třídy složitosti a odpovídající důkaz opět naleznete v \cite{TIN}. Netriviální problémy spadající do této třídy složitosti není možné řešit běžnými algoritmy na současném HW v~rozumném čase.
Tato práce se zabývá řešením SAT problému pomocí tzv. \textit{genetického algoritmu}, díky kterému je možné řešit (některé) instance tohoto problému ve výrazně kratším čase, než který odpovídá teoretické složitosti. Nevýhodou tohoto přístupu je, že není zaručeno, že bude řešení nalezeno v konečném čase, pokud existuje\footnote{Experimentálně však bylo zjištěno, že při vhodně zvolených parametrech, se řešení \textit{většinou} najde. Za~určitých předpokladů lze navíc matematicky dokázat, že genetický algoritmus nalezne existující řešení v~nekonečném čase.}.
Vytvořený program dokáže zadaný SAT problém řešit jak pomocí genetického algoritmu, tak pomocí běžného \textit{(slepého)} algoritmu. V závěru práce jsou tyto přístupy porovnány na různých instancích SAT problému. Kompletní zdrojové kódy a programovou dokumentaci je možné stáhnout z \href{http://dudka.cz/fss}{{\tt http://dudka.cz/fss}}.
\section{Poděkování}
Software použitý v této práci používá knihovnu genetických algoritmů \texttt{GAlib}, kterou napsal Matthew Wall z Massachusetts Institute of Technology.
\chapter{Teoretická část}\label{theory}
\section{Genetický algoritmus}
Citace z \cite{Kvas}:
\begin{quote}
Genetický algoritmus patří mezi základní stochastické optimalizační algoritmy s výraznými evolučními rysy. V současnosti je nejčastěji používaným evolučním optimalizačním algoritmem, se širokou paletou aplikací od optimalizace vysoce multimodálních funkcí přes kombinatorické a grafově-teoretické problémy až po~aplikace nazývané \quotedblbase{umělý život\textquotedblleft}.
Ukazuje se, že na základě analogie s evolučními procesy probíhajícími v biologických systémech existuje alternativní možnost, jak usměrnit náhodné gene\-rování bodů k hodnotám blízkým optimálním. Právě tato analogie se stala základem \textit{genetického algoritmu}, který vylepšuje čistý stochastický slepý algoritmus tak, že poskytuje v reálném čase optimální řešení.
Darwinova teorie evoluce se zakládá na tezi \textit{přirozeného výběru}, podle které přežívají jen nejlépe přizpůsobení jedinci populace. \textit{Reprodukcí} dvou jedinců s~vysokým \textit{fitness} dostáváme potomky, kteří budou s vysokou pravděpodobností dobře přizpůsobení na úspěšné přežití. Při podrobné analýze (hlavně matematické) se ukazuje, že samotné působení reprodukce není dostatečně efektivní na vznik dobře přizpůsobených jedinců s novými vlastnostmi, které významně ulehčují přežití. Do evoluce živé hmoty je nutné zapojit i tzv. \textit{mutace}. Tyto mutace ovlivňují náhodným způsobem (kladně nebo záporně) genetický materiál populace jedinců.
Biologická evoluce je progresivní změna obsahu genetické informace (\textit{genotypu}) populace v průběhu několika generací. Zavádí se pojem \textit{fitness}, který hraje klíčovou úlohu v úvahách o genetickém algoritmu. V biologii je fitness definovaná jako relativní schopnost přežití a reprodukce genotypu v daném prostředí. Podobně se chápe i v umělém živote, je to kladné číslo přiřazené genetické informaci repreprezentující organizmus (obvykle vyjádřené pomocí bitového řetězce), které reprezentuje jeho relativní úspěšnost plnit si v daném prostředí svoje úlohy (např. sběr potravy) a vstupovat do reprodukce, t.j. tvořit nové organizmy.
\end{quote}
\section{Knihovna \texttt{GAlib}}
\texttt{GAlib} je C++ knihovna, která obsahuje komponenty pro tvorbu genetických algoritmů. Zahrnuje nástroje pro použití genetických algoritmů k optimalizacím v různých C++ programech, které mohou využívat jakoukoliv reprezentaci a genetické operátory. \texttt{GAlib} je podporován na různých UNIX platformách (Linux, MacOSX, SGI, Sun, HP, DEC, IBM) stejně dobře jako na MacOS a DOS/Windows systémech. Knihovnu lze stáhnout\\z \href{http://lancet.mit.edu/ga/}{http://lancet.mit.edu/ga/}.
\chapter{Návrh řešení}\label{design}
Hlavním cílem návrhu byla znovupoužitelnost\cite{Gamma}\cite{Pecin}\cite{Stroustrup}\cite{Sutter}. Většina modulů nemá žádné exter\-ní závislosti. Pokud bychom např. místo knihovny \texttt{GAlib} chtěli použít jinou knihovnu, stačilo by nadefinovat dvě nové třídy pracující se stávajícím objektovým modelem. Program je z hlediska návrhu dělen do několika částí:
\begin{itemize}
\item \textbf{Reprezentace problému} - modul \texttt{SatProblem}
\item \textbf{Abstrakce prohledávače, observery} - modul \texttt{SatSolver}
\item \textbf{Implementace prohledávače} - moduly \texttt{GaSatSolver} a \texttt{BlindSatSolver}
\end{itemize}
\section{Vstupních data}
Z matematického pohledu je instance problému definována jako množina formulí výrokové logiky. Tyto formule tedy tvoří vstupní data programu a je potřeba je programu nějak předat. K tomuto účelu byl vytvořen jednoduchý jazyk pro zápis výrokových formulí, kterému program rozumí.
Tento jazyk je podmnožinou jazyka pro zápis logických výrazů v C++. Výrokové proměn\-né jsou pojmenovány pomocí identifikátorů. Identifikátor je jakákoliv sekvence písmen, číslic a znaku podtržítko, přičemž musí začínat písmenem nebo podtržítkem. Dále jazyk obsahuje binární operátory, unární operátor negace a závorky. Jednotlivé formule jsou od~sebe odděleny středníkem. Lexikální prvky jazyka jsou shrnuty v tabulce \ref{lexTable}. Stejně jako C++ je i tento jazyk \textit{case-sensitive}.
\begin{table}[h]
\begin{center}
\begin{small}
\begin{tabular}{|l|l|l|}\hline
Znaková reprezentace&Alternativní reprezentace&Sémantika\\\hline
\&&AND&konjunkce (binární operátor)\\
$\mid$&OR&disjunkce (binární operátor)\\
\begin{Large}\verb|^|\end{Large}&XOR&exclusive OR (binární operátor)\\
$\sim$&NOT&negace (unární operátor)\\
(~)&&závorky\\
0&FALSE&nepravda\\
1&TRUE&pravda\\
\verb|[a-zA-Z_][a-zA-Z0-9_]|&&identifikátor\\
;&&středník - oddělovač formulí\\\hline
\end{tabular}
\end{small}
\end{center}
\caption{Lexikální prvky jazyka pro zápis výrokových formulí}
\label{lexTable}
\end{table}
\section{Interní reprezentace problému}
Definice problému pomocí jazyka je vhodná pro uživatele, ale není příliš vhodná pro zpracování genetickým algoritmem. Navíc operace vyhodnocení jednotlivých formulí je časově kritická část výpočtu. Proto si program na základě vstupních dat vytváří interní reprezentaci problému založenou na objektech C++.
Diagram tříd, které zajišťují převod vstupních dat na interní reprezentaci, je zachycen na~obr.~\ref{parser}. Na tomto diagramu je znázorněno využití návrhového vzoru \textit{decorator}. Výsled\-kem zpracování vstupu je množina načtených názvů proměnných a množina načtených výrokových formulí. Tato data jsou uložena v kontejnerech \texttt{VariableContainer} a \texttt{Formula\-Container}.
\begin{figure}[h]
\begin{center}\includegraphics[scale=0.5]{parser.png}\end{center}
\caption{Zpracování vstupních dat - objektový model}\label{parser}
\end{figure}
Načítání problému ze vstupního souboru je považováno pouze za jednu z variant, jak problém definovat. Proto je interní reprezentace dat zcela oddělena od algoritmů, které s daty pracují. Toho je docíleno pomocí tzv. \textit{rozhraní}\footnote{Rozhraní (\textit{interface}) je z pohledu překladače C++ čistě abstraktní třída (\textit{pure virtual}).}. Rozhraní \texttt{IFormulaEvaluator} představuje vyhodnotitelnou výrokovou formuli a rozhraní \texttt{ISatItem} její ohodnocení. Defi\-nici problému jako celek zpřístupňuje objekt \textit{SatProblem} (návrhový vzor \textit{Facade}). Situace je znázorněna na diagramu \ref{SatProblem}.
\begin{figure}[h]
\begin{center}\includegraphics[scale=0.5]{SatProblem.png}\end{center}
\caption{Interní reprezentace SAT problému - objektový model}\label{SatProblem}
\end{figure}
\section{Abstrakce prohledávače}
Jak bylo naznačeno v úvodu, program umožňuje řešit daný SAT problém dvěma způsoby -- pomocí genetického algoritmu a pomocí slepého prohledávače. Abstraktní třída \texttt{Abstract\-SatSolver} definuje společné rozhraní pro oba prohledávače. Tuto třídu lze také použít jako bázovou třídu pro definici jakéhokoliv prohledávače, např. pro využití jiné knihovny než je \texttt{GAlib}.
Definice společného rozhraní je důležitá pro spolupráci s \textit{observery}. Observery jsou objekty, které mohou sledovat aktuální stav prohledávače a nějak reagovat na změny tohoto stavu -- např. tím, že vypisují informace o průběhu prohledávání, nebo vyhodnocují podmínky pro zastavení prohledávače.
Třída \texttt{AbstractSatSolver} proto implementuje několik rozhraní, které mohou observery využívat při práci s prohledávačem. Nejdůležitější z nich je rozhraní \texttt{ISubject} na samém vrcho\-lu hierarchie dědičnosti, které umožňuje jednotlivé observery k prohledávači připojovat. Hierarchie dědičnosti je znázorněna na obr. \ref{ASSinheritance}.
\begin{figure}[h]
\begin{center}\includegraphics[scale=0.5]{ASSinheritance.png}\end{center}
\caption{Hierarchie dědičnosti třídy \texttt{AbstractSatSolver}}\label{ASSinheritance}
\end{figure}
\section{Observery}
Observery jsou navrženy tak, aby byly pokud možno nezávislé na konkrétním typu prohle\-dávače. Observery implementované v současné verzi aplikace se starají pouze o výpis potřeb\-ných informací do konzole a případné ukončení prohledávání při splnění uživatelem definovaných podmínek. Spolupráci prohledávače s observery znázorňuje znázorňuje diagram tříd na obr. \ref{AbstractSatSolver}. Seznam jednotlivých observerů je uveden v tabulce \ref{tabObservers}.
\begin{figure}[h]
\begin{center}\includegraphics[scale=0.5]{SatSolver.png}\end{center}
\caption{Spolupráce prohledávače s observery}\label{AbstractSatSolver}
\end{figure}
\begin{table}[h]
\begin{center}
\begin{small}
\begin{tabular}{|r|l|}\hline
Třída&Chování\\\hline
\texttt{TimedStop}&Zastaví prohledávání po uplynutí předem daného času.\\
\texttt{SolutionsCountStop}&Zastaví prohledávání, pokud je nalezen požadovaný počet řešení.\\
\texttt{ProgressWatch}&Průběžně vypisuje informace o průběhu prohledávání.\\
\texttt{ResultsWatch}&Průběžně vypisuje nalezená řešení.\\
\texttt{FitnessWatch}&Zobrazuje informace, pokud bylo nalezeno ohodnocení s vyšší hodnotou \textit{fitness}.\\\hline
\end{tabular}
\end{small}
\end{center}
\caption{Seznam observerů a jejich chování}
\label{tabObservers}
\end{table}
Pro jednodušší práci s observery byla vytvořena C++ šablona, která observer vytvoří s~požadovanými parametry a zároveň jej připojí ke sledovanému objektu:
\begin{verbatim}
// Create observer OBSERVER and attach it to subject
template <
class OBSERVER,
class SUBJECT,
class ARG>
inline OBSERVER* createAttached(SUBJECT *subject, ARG &arg) {
OBSERVER *observer= new OBSERVER(subject, arg);
subject->addObserver(observer);
return observer;
}
\end{verbatim}
Samotný zápis kódu přidávající jednotlivé observery pak vypadá mnohem přehledněji, přičemž není nijak omezeno původní rozhraní observeru. Lze tedy kombinovat oba dva způsoby připojení observeru:
\begin{verbatim}
// attach progress indicator
const int progressBits = satProblem->getVarsCount()-stepWidth;
if (progressBits > 0) {
progressWatch = new ProgressWatch(satSolver, 1<<progressBits, std::cout);
satSolver->addObserver(progressWatch);
}
// Display message if maxFitness is increased
fitnessWatch = createAttached<FitnessWatch>(satSolver, std::cout);
\end{verbatim}
\section{Jednotlivé implementace prohledávače}
Jak bylo zmíněno v úvodu, program poskytuje dvě implementace prohledávače, mezi kterými lze přepínat -- slepý prohledávač a prohledávač využívající genetický algoritmus. V tabul\-ce~\ref{tabAdvantages} jsou shrnuty výhody a nevýhody obou implementací. Třídy implementující tyto prohledávače se jmenují \texttt{BlindSatSolver} a \texttt{GaSatSolver}.
\begin{table}[h]
\begin{center}
\begin{scriptsize}
\begin{tabular}{|l|l|}\hline
Slepý prohledávač&GA prohledávač\\\hline
\texttt{+} dokáže nalézt všechna existující řešení&\texttt{-} není zaručeno, že najde všechna řešení\\
\texttt{+} čas potřebný k prohledávání lze spočítat předem&\texttt{-} nelze obecně definovat podmínky zastavení\\
\texttt{-} vhodný pouze pro triviální problémy&\texttt{+} dokáže řešit složité problémy na běžné arch.\\
\texttt{-} asymptotická časová složitost je exponenciální&\texttt{+} většinou nalezne řešení velmi rychle, pokud existuje\\
\texttt{-} počet proměnných je omezen architekturou počítače&\texttt{-} pro určité třídy problémů je potřeba upravit řídící parametry\\\hline
\end{tabular}
\end{scriptsize}
\end{center}
\caption{Srovnání výhod a nevýhod obou implementací prohledávačů}
\label{tabAdvantages}
\end{table}
Implementace slepého prohledávače je velmi jednoduchá. Ohodnocení jednotli\-vých pro\-měnných se ukládá jako celé číslo. Tím je zaručeno efektivní zpracování pomocí aritmetických a bitových operací nad tímto typem. Prohledávací smyčka provádí pouze inkrementaci tohoto čísla a vyhodnocení výrokových formulí. Počet výrokových proměnných je v tomto případě omezen přibližně na \texttt{sizeof(long)} dané architektury. To však v praxi příliš nevadí, protože pro složitější problémy je slepý prohledávač stejně nepoužitelný.
Třída \texttt{GaSatSolver} funguje jako propojení knihovny \texttt{GAlib} se zbytkem programu.\\ Na~obr.~\ref{GaSatSolver} je znázorněn graf spolupráce této třídy. Tato třída pouze implementuje rozhraní prohledávače pomocí tříd knihovny \texttt{GAlib}. Používá genetický algoritmus definovaný třídou \texttt{GASimpleGA}. Během experimentů byly porovnávány i jiné algoritmy - viz. kapitola \ref{results}. Pro použití jiného algoritmu stačí (díky kvalitnímu objektovému modelu knihovny \texttt{GAlib}) změnit jediný řádek v programu\footnote{Nebyl by problém změnit program tak, aby bylo možné jednotlivé genetické algoritmy přepínat za běhu. Experimenty však ukázaly, že to samo o sobě nepřinese velký užitek.}.
\begin{figure}[h]
\begin{center}\includegraphics[scale=0.5]{GaSatSolver.png}\end{center}
\caption{Graf spolupráce třídy \texttt{GaSatSolver}}\label{GaSatSolver}
\end{figure}
Pro kódování chromozómu byla použita třída \texttt{GA1DBinaryStringGenome}, která kóduje jedince jako jednorozměrné bitové řetězce. K zjištění hodnoty \textit{fitness} jedince je potřeba provést nad ním vyhodnocení všech formulí -- je tedy potřeba tyto objekty \textit{obalit}, aby implementovali dříve definované rozhraní \texttt{ISatItem}. K tomu slouží třídy \texttt{GaSatItem} a~\texttt{SatItem\-GalibAdatper}, přičemž druhá z nich pracuje pouze s odkazem na objekty knihovny \texttt{GAlib} (z~důvodu optimalizace). Plnohodnotná implementace je zase potřeba pro tvoření kontej\-nerů (množina, vektor, ...).
Hodnota \textit{fitness} se počítá podle následujícího vztahu:
\begin{displaymath}
fitness=\frac{satisfied~formula~count}{total~formula~count}
\end{displaymath}
Hodnota tedy leží v intervalu $\langle0,1\rangle$. $0$ znamená, že není splněna ani jedna formule, $1$ znamená, že jsou splněny všechny formule (nalezeno řešení).
Nalezená řešení jsou ukládána vně knihovny \texttt{GAlib} pomocí kontejneru \textit{množina} -- třídy \texttt{SatItemSet}. Tento kontejner zajistí, aby každé ohodnocení proměnných (nalezené řešení) bylo v kontejneru právě jednou. Tím lze sledovat celkový počet nalezených (navzájem různých) řešení a nakonec je všechny vypsat.
\chapter{Implementace}\label{implementation}
Program je implementovaný v jazyce C++, většinu jeho modulů lze kompilovat bez exter\-ních závislostí. Pouze moduly \texttt{GaSatSolver} a \texttt{fss} (modul obsahující funkci \texttt{main}) jsou závislé na knihovně \texttt{GAlib}. Spustitelný soubor se jmenuje \texttt{fss}. Přehled parametrů je uveden v tabulce \ref{tabArgs}. Jednotlivé parametry se zadávají vždy jako pár název---hodnota. Pokud zvolíte GA prohledávač, je možné zadat i další parametry, které zpracovává \texttt{GAlib} -- tyto parametry nejsou uvedeny v tabulce. Podrobnosti naleznete v dokumentaci ke knihovně \texttt{GAlib} a její třídě \texttt{GASimpleGA}.
\begin{table}[h]
\begin{center}
\begin{small}
\begin{tabular}{|l|l|l|}\hline
Název parametru&Zkrácený název&Sémantika\\\hline
\texttt{input\_file}&\texttt{input}&Vstupní soubor obsahující definici SAT problému.\\
&&Znak \quotedblbase{-\textquotedblleft} představuje standardní vstup.\\\hline
\texttt{color\_output}&\texttt{color}&\texttt{1/0} zapíná/vypíná barevný konzolový výstup.\\\hline
\texttt{verbose\_mode}&\texttt{verbose}&\texttt{1/0} zapíná/vypíná kontrolní výstup knihovny GAlib.\\\hline
\texttt{blind\_solver}&\texttt{blind}&Přepíná mezi slepým a GA prohledávačem.\\
&& 1 zapíná slepý prohledávač.\\
&& 0 zapíná GA prohledávač (výchozí).\\\hline
\texttt{step\_width}&\texttt{stepw}&\textit{(jenom pro slepý prohledávač)}\\
&& Granularita oznamování a řízení prohledávače.\\
&& Výchozí hodnota je 16.\\\hline
\texttt{min\_count\_of\_solutions}&\texttt{minslns}&Minimální požadovaný počet řešení.\\\hline
\texttt{max\_count\_of\_solutions}&\texttt{maxslns}&Maximální počet hledaných řešení.\\\hline
\texttt{max\_count\_of\_runs}&\texttt{maxruns}&Maximální počet opakování běhu GA,\\
&& pokud není nalezen požadovaný počet řešení.\\\hline
\texttt{max\_time\_per\_run}&\texttt{maxtime}&Běh je bezpodmínečně přerušen pokud je překročen\\
&& daný čas (v milisekundách).\\\hline
\texttt{term\_upon\_convergence}&\texttt{convterm}&\texttt{0 -> }Běh GA je přerušen po \texttt{ngen} generacích.\\
&& \texttt{1 -> }Běh GA je přerušen podle kritéria konvergence.\\\hline
\end{tabular}
\end{small}
\end{center}
\caption{Přehled parametrů programu \texttt{fss}}
\label{tabArgs}
\end{table}
\section{Sestavení ze zdrojových kódů}
Z webu projektu \href{http://dudka.cz/fss}{http://dudka.cz/fss} lze stáhnout archiv obsahující zdrojové kódy projektu spolu se zdrojovými kódy knihovny \texttt{GAlib}. Součástí archivu je \texttt{Makefile}, který zajistí sestavení knihovny \texttt{GAlib}, přeložení zdrojového kódu aplikace a jeho slinkování s~knihovnou.
Program používá automatický \textit{build-systém} \texttt{CMake}, který detekuje závislosti mezi moduly, závislosti na systémové knihovny, překladač apod. Pro distribuci Gentoo Linux lze na webu projektu stáhnout \textit{ebuild}, který zajistí automatické stažení, sestavení a instalaci včetně všech závislostí.
Nedílnou součástí dokumentace je dokumentace API, kterou lze vygenerovat pomocí programu \texttt{Doxygen} -- vše potřebné je v adresáři \texttt{doc/api}. Tuto dokumentaci lze také, stejně jako zdrojové kódy, najít na webu projektu. Na obrázku \ref{screenshot} je ukázka použití programu.
\begin{figure}[h]
\begin{center}\includegraphics[scale=0.5]{screenshot.png}\end{center}
\caption{Ukázka použití programu}\label{screenshot}
\end{figure}
\chapter{Výsledky}\label{results}
Hlavní překážkou při testování programu byl nedostatek testovacích dat. Jinými slovy nepodařilo se mi sehnat vhodné zadání SAT problému, na kterém bych prohledávač otestoval. Vytvořil jsem si proto generátor náhodných SAT problémů -- program \texttt{fss-satgen}. Tento program je také součástí archivu a je velmi jednoduchý. Jako parametry se mu zadají počet výrokových proměnných a počet formulí, které z nich má sestavit. Výstupem je množina náhodně vygenerovaných výrokových formulí zapsaných v jazyku, kterému rozumí prohledávač.
Nevýhodou takového přístupu je skutečnost, že u takto vygenerovaného problému ne\-máme předem informaci o tom, jestli má nějaké řešení, popř. kolik má řešení. Pro jednodušší problémy (obvykle max. 20 -- 30 výrokových proměnných) je možné na problém pustit nejprve slepý prohledávač. Výstupem slepého prohledávače je přesná informace o počtu řešení. Stejný problém potom můžeme předhodit GA prohledávači a porovnat čas, který potřebuje k jeho vyřešení. Tohle byl hlavní směr, kterým se testování ubíralo.
Kromě klasického genetického algoritmu (tak jak jej implementuje \texttt{GAlib}) bylo implementováno automatické restartování běhu GA v případě, že byly splněny podmínky pro~ukončení běhu a zároveň nebyl nalezen požadovaný počet řešení. Tohle nepatrné vy\-lepšení se ukázalo jako velmi přínosné pro snížení času prohledávání.
Bylo zjištěno, že program nalezne požadovaný počet řešení mnohem rychleji, pokud má předem informaci o počtu řešení. Takového chování dosáhneme specifikací parametrů \texttt{minslns} a \texttt{maxslns} (viz. obr. \ref{screenshot}). Horní ohraničení umožňuje zastavit GA při dosažení daného počtu řešení. Zatímco dolní ohraničení umožňuje restartovat běh, pokud nevede k~cíli. Tyto parametry se obecně mohou lišit.
Co se týká klasických parametrů GA, výraznější zlepšení bylo dosaženo upravením veli\-kosti populace pro některé problémy. U problémů, které měly hodně řešení, byla řešení nalezena rychleji při nastavení menší velikosti populace. U jednoho testovaného problému, který měl více než 12000 řešení, se jako optimální hodnota ukázala velikost populace dokonce jenom 30 jedinců.
Asi nejdůležitějším parametrem byl počet generací jako ukončovací kritérium běhu. Kromě ukončení po daném počtu generací je možné ukončit běh podle konvergenčního kritéria tak, jak jej definuje \texttt{GAlib}. Nejzajímavější z pohledu uživatele je asi ukončení běhu po uplynutí předem daného času. Tohle ukončení lze kombinovat s ostatními kritérii a zaručuje ukončení výpočtu v uživatelem stanoveném čase bez ohledu na počet nalezených řešení.
Program byl testován na různých SAT problémech různé složitosti -- jak počet proměn\-ných, tak počet formulí dosahovali řádu stovek. V tabulce \ref{tabTime} je nastíněna závislost času prohledávání na použitých parametrech. Pro vytvoření této tabulky byl jako vstup použit jednoduchý SAT problém s 20ti proměnnými a 20ti formulemi -- díky tomu bylo možné použít slepý i GA prohledávač.
\begin{table}[h]
\begin{center}
\begin{small}
\begin{tabular}{|l|r|r|}\hline
Parametry prohledávání&Počet nalezených řešení&Doba prohledávání\\\hline
\textit{bez parametru}&3 -- 6&1.29 s\\
\texttt{ngen 500}&5 -- 6&2.58 s\\
\texttt{minslns 6}&6&1.29 -- 5.19 s\\
\texttt{minslns 6 maxslns 6}&6&0.60 -- 5.19 s\\
\texttt{minslns 6 maxslns 6 time 1000 maxruns 1}&0 -- 6&0.60 -- 1.01 s\\\hline
\texttt{blind 1}&6&116.07 s\\
\texttt{blind 1 maxslns 6}&6&92.03 s\\
\texttt{blind 1 maxtime 60000 stepw 10}&4&60.12 s\\\hline
\end{tabular}
\end{small}
\end{center}
\caption{Závislost doby prohledávání na parametrech}
\label{tabTime}
\end{table}
\chapter{Závěr}
Cílem návrhu bylo vytvořit znovupoužitelné komponenty pro řešení SAT problému. Tyto komponenty byly propojeny s již hotovou a odladěnou knihovnou \texttt{GAlib} a tím bylo dosaženo vysoké efektivity řešení SAT problému pomocí genetického algoritmu. Za nejvýznamnější výsledky práce považuji srovnání běžného postupu řešení s GA z hlediska časové náročnosti a použitelnosti pro daný problém.
Ukázalo se, že pomocí GA je možné řešit problémy, které by jinak nebyly vůbec řešitelné na současném HW. Kromě toho vznikla plnohodnotná aplikace, která umožňuje SAT problé\-my řešit. Nezanedbatelný je i můj osobní přínos -- seznámení se s knihovnou \texttt{GAlib}, která má mnohem širší obor využití, než kterým se zabývá tato práce.
% ----------------------------------------------
% Použitá literatura
\bibliographystyle{./czechiso}
\begin{flushleft}
\bibliography{proj_doc}
\end{flushleft}
\end{document}
Back to main page
proj_doc_content.tex [Download]