\relax 
\@writefile{toc}{\contentsline {chapter}{Abstrakt}{i}}
\@writefile{toc}{\contentsline {chapter}{Seznam obr\'azk\r u}{v}}
\@writefile{toc}{\contentsline {chapter}{Seznam tabulek}{vii}}
\citation{cook}
\citation{satcomp}
\citation{satlive}
\@writefile{toc}{\contentsline {chapter}{\numberline {1}\'Uvod}{1}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\@writefile{toc}{\contentsline {section}{\numberline {1.1}Probl\'em splnitelnosti (SAT)}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {1.2}Open-Source SAT solvery}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {1.3}\v Clen\v en\IeC {\'\i } pr\'ace}{2}}
\@writefile{toc}{\contentsline {chapter}{\numberline {2}SAT algoritmy}{3}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{chap:satalg}{{2}{3}}
\@writefile{toc}{\contentsline {section}{\numberline {2.1}Teoretick\'y \'uvod}{3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1.1}Booleovsk\'a formule}{3}}
\newlabel{exp1}{{2.1.1}{3}}
\newlabel{exp2}{{2.1.2}{3}}
\citation{dp}
\citation{dll}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1.2}Resoluce}{4}}
\newlabel{resol}{{2.1.2}{4}}
\newlabel{prop1}{{2.1.1}{4}}
\newlabel{eq:eq1}{{2.1}{4}}
\@writefile{toc}{\contentsline {section}{\numberline {2.2}Stru\v cn\'y p\v rehled \v re\v sen\IeC {\'\i } SAT probl\'emu}{5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.1}DP algoritmus}{5}}
\citation{dpalg}
\@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces Rekurzivn\IeC {\'\i } DP algoritmus}}{6}}
\newlabel{fig:DP}{{2.1}{6}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces Stavov\'y prostor SAT probl\'emu}}{7}}
\newlabel{fig:tree}{{2.2}{7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.2}DLL algoritmus}{7}}
\newlabel{ssec:DLL}{{2.2.2}{7}}
\citation{bdd}
\citation{bdd}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.3}Binary Decision Diagrams}{9}}
\newlabel{ssec:bdd}{{2.2.3}{9}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.3}{\ignorespaces Iterativn\IeC {\'\i } podoba DLL algoritmu}}{10}}
\newlabel{fig:iterDLL}{{2.3}{10}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.4}{\ignorespaces Jednoduch\'y ROBDD}}{10}}
\newlabel{fig:bdd}{{2.4}{10}}
\citation{stalmarck}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.4}St\r almarck\r uv algoritmus}{11}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.5}Stochastick\'e algoritmy}{12}}
\citation{localsearch}
\@writefile{lof}{\contentsline {figure}{\numberline {2.5}{\ignorespaces Minimalizace c\IeC {\'\i }lov\'e funkce}}{13}}
\newlabel{fig:locsearch}{{2.5}{13}}
\citation{walksat}
\citation{hoos}
\@writefile{toc}{\contentsline {section}{\numberline {2.3}Sou\v casn\'e SAT solvery}{14}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.1}WalkSAT}{14}}
\newlabel{ssec:walksat}{{2.3.1}{14}}
\citation{chaff}
\@writefile{lof}{\contentsline {figure}{\numberline {2.6}{\ignorespaces Local search algoritmus WalkSATu}}{15}}
\newlabel{fig:walksat}{{2.6}{15}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.2}zChaff}{15}}
\newlabel{ssec:zchaff}{{2.3.2}{15}}
\@writefile{toc}{\contentsline {subsubsection}{Strategie ur\v cen\IeC {\'\i } prom\v enn\'e}{15}}
\@writefile{toc}{\contentsline {subsubsection}{BCP engine}{16}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.7}{\ignorespaces Two Literal Watching sch\'ema}}{16}}
\newlabel{fig:2watch}{{2.7}{16}}
\citation{grasp}
\@writefile{toc}{\contentsline {subsubsection}{Anal\'yza konfliktu a u\v cen\IeC {\'\i }}{17}}
\citation{minisat}
\citation{rsat}
\citation{nanosat}
\citation{jerusat}
\citation{balcarek}
\@writefile{lof}{\contentsline {figure}{\numberline {2.8}{\ignorespaces Typick\'y implika\v cn\IeC {\'\i } graf}}{18}}
\newlabel{fig:UIP}{{2.8}{18}}
\@writefile{toc}{\contentsline {subsubsection}{Restarty}{18}}
\citation{force}
\citation{ve}
\citation{satcomp}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.3}EBDDRES}{19}}
\newlabel{ssec:ebddres}{{2.3.3}{19}}
\citation{bench}
\@writefile{toc}{\contentsline {section}{\numberline {2.4}Srovn\'an\IeC {\'\i } SAT solver\r u}{20}}
\newlabel{sec:testing}{{2.4}{20}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.4.1}Pou\v zit\'e benchmarky}{20}}
\newlabel{ssec:bench}{{2.4.1}{20}}
\@writefile{lot}{\contentsline {table}{\numberline {2.1}{\ignorespaces Pou\v zit\'e benchmarky}}{20}}
\newlabel{tab:bench}{{2.1}{20}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.4.2}Porovn\'an\IeC {\'\i } heuristik WalkSATu}{21}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.4.3}Porovn\'an\IeC {\'\i } heuristik EBDDRESu}{21}}
\newlabel{RF1}{{2.4.2}{22}}
\@writefile{lot}{\contentsline {table}{\numberline {2.2}{\ignorespaces Srovn\'an\IeC {\'\i } heuristik WalkSATu}}{22}}
\newlabel{tab:walkheur}{{2.2}{22}}
\citation{gensat}
\@writefile{lot}{\contentsline {table}{\numberline {2.3}{\ignorespaces Vliv po\v ctu prom\v enn\'ych na v\'ykon EBDDRESu}}{23}}
\newlabel{tab:ebddrestest1}{{2.3}{23}}
\@writefile{lot}{\contentsline {table}{\numberline {2.4}{\ignorespaces Vliv po\v ctu klauzul\IeC {\'\i } na v\'ykon EBDDRESu}}{23}}
\newlabel{tab:ebddrestest2}{{2.4}{23}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.4.4}V\'ysledky srovn\'an\IeC {\'\i } SAT solver\r u}{23}}
\newlabel{RF2}{{2.4.3}{24}}
\@writefile{lot}{\contentsline {table}{\numberline {2.5}{\ignorespaces Srovn\'an\IeC {\'\i } heuristik EBDDRESu}}{24}}
\newlabel{tab:ebddresheur}{{2.5}{24}}
\citation{gensat}
\@writefile{lot}{\contentsline {table}{\numberline {2.6}{\ignorespaces Srovn\'an\IeC {\'\i } jednotliv\'ych SAT solver\r u}}{25}}
\newlabel{tab:solvercompare}{{2.6}{25}}
\@writefile{lot}{\contentsline {table}{\numberline {2.7}{\ignorespaces Vliv po\v ctu prom\v enn\'ych na v\'ykon SAT solver\r u}}{25}}
\newlabel{tab:solvertest1}{{2.7}{25}}
\@writefile{lot}{\contentsline {table}{\numberline {2.8}{\ignorespaces Vliv po\v ctu klauzul\IeC {\'\i } na v\'ykon SAT solver\r u}}{26}}
\newlabel{tab:solvertest2}{{2.8}{26}}
\@writefile{lot}{\contentsline {table}{\numberline {2.9}{\ignorespaces Vliv pom\v eru po\v ctu klauzul\IeC {\'\i } ku po\v ctu prom\v enn\'ych}}{26}}
\newlabel{tab:solvertest3}{{2.9}{26}}
\@writefile{toc}{\contentsline {chapter}{\numberline {3}Modifikace SAT algoritm\r u}{27}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\@writefile{toc}{\contentsline {section}{\numberline {3.1}Modifikace ROBDD}{27}}
\newlabel{exp3}{{3.1.1}{28}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.1}{\ignorespaces Obr\'azek k p\v r\IeC {\'\i }kladu (1)}}{28}}
\newlabel{fig:bdddc1}{{3.1}{28}}
\@writefile{toc}{\contentsline {section}{\numberline {3.2}Modifikace WalkSAT algoritmu}{28}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.2}{\ignorespaces Obr\'azek k p\v r\IeC {\'\i }kladu (2)}}{29}}
\newlabel{fig:bdddc2}{{3.2}{29}}
\newlabel{exp4}{{3.2.1}{29}}
\@writefile{toc}{\contentsline {section}{\numberline {3.3}Modifikace DLL algoritmu}{30}}
\newlabel{sec:modDLL}{{3.3}{30}}
\citation{dimacs}
\@writefile{toc}{\contentsline {section}{\numberline {3.4}DCSAT}{31}}
\newlabel{sec:dcsat}{{3.4}{31}}
\citation{gensat}
\citation{toman}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4.1}Testov\'an\IeC {\'\i } DCSATu}{32}}
\@writefile{lot}{\contentsline {table}{\numberline {3.1}{\ignorespaces Srovn\'an\IeC {\'\i } MiniSatu a DCSATu}}{32}}
\newlabel{tab:dcsattest1}{{3.1}{32}}
\@writefile{lot}{\contentsline {table}{\numberline {3.2}{\ignorespaces Porovn\'an\IeC {\'\i } DCSATu s BoolToolem}}{33}}
\newlabel{tab:dcsat2booltool}{{3.2}{33}}
\@writefile{lot}{\contentsline {table}{\numberline {3.3}{\ignorespaces Vliv po\v ctu prom\v enn\'ych na v\'ykon DCSATu (1)}}{33}}
\newlabel{tab:dcsattest2a}{{3.3}{33}}
\@writefile{lot}{\contentsline {table}{\numberline {3.4}{\ignorespaces Vliv po\v ctu prom\v enn\'ych na v\'ykon DCSATu (2)}}{34}}
\newlabel{tab:dcsattest2b}{{3.4}{34}}
\@writefile{lot}{\contentsline {table}{\numberline {3.5}{\ignorespaces Vliv po\v ctu klauzul\IeC {\'\i } na v\'ykon DCSATu (1)}}{34}}
\newlabel{tab:dcsattest3a}{{3.5}{34}}
\@writefile{lot}{\contentsline {table}{\numberline {3.6}{\ignorespaces Vliv po\v ctu klauzul\IeC {\'\i } na v\'ykon DCSATu (2)}}{34}}
\newlabel{tab:dcsattest3b}{{3.6}{34}}
\@writefile{lot}{\contentsline {table}{\numberline {3.7}{\ignorespaces Vliv pom\v eru klauzul\IeC {\'\i }/prom\v enn\'ych na v\'ykon DCSATu}}{35}}
\newlabel{tab:dcsattest4}{{3.7}{35}}
\@writefile{toc}{\contentsline {chapter}{\numberline {4}Z\'av\v er}{37}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\bibstyle{plain}
\bibdata{ref}
\bibcite{bench}{1}
\bibcite{dimacs}{2}
\bibcite{dpalg}{3}
\bibcite{satcomp}{4}
\bibcite{satlive}{5}
\bibcite{rsat}{6}
\bibcite{gensat}{7}
\bibcite{force}{8}
\bibcite{balcarek}{9}
\bibcite{nanosat}{10}
\bibcite{bdd}{11}
\bibcite{cook}{12}
\bibcite{dll}{13}
\bibcite{dp}{14}
\bibcite{minisat}{15}
\bibcite{hoos}{16}
\bibcite{ve}{17}
\bibcite{grasp}{18}
\bibcite{walksat}{19}
\bibcite{chaff}{20}
\bibcite{jerusat}{21}
\bibcite{localsearch}{22}
\bibcite{stalmarck}{23}
\bibcite{toman}{24}
\@writefile{toc}{\contentsline {chapter}{Literatura}{40}}
\citation{minisat}
\@writefile{toc}{\contentsline {chapter}{\numberline {A}Manu\'al DCSATu}{41}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\@writefile{toc}{\contentsline {section}{\numberline {A.1}Nov\'e funkce}{41}}
\@writefile{toc}{\contentsline {section}{\numberline {A.2}Instalace a u\v z\IeC {\'\i }v\'an\IeC {\'\i }}{42}}
\@writefile{toc}{\contentsline {chapter}{\numberline {B}Obsah CD}{43}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\@writefile{lof}{\contentsline {figure}{\numberline {B.1}{\ignorespaces Obsah p\v rilo\v zen\'eho CD}}{43}}
\newlabel{fig:cd}{{B.1}{43}}
