\contentsline {chapter}{Abstrakt}{i}
\contentsline {chapter}{Seznam obr\'azk\r u}{v}
\contentsline {chapter}{Seznam tabulek}{vii}
\contentsline {chapter}{\numberline {1}\'Uvod}{1}
\contentsline {section}{\numberline {1.1}Probl\'em splnitelnosti (SAT)}{1}
\contentsline {section}{\numberline {1.2}Open-Source SAT solvery}{2}
\contentsline {section}{\numberline {1.3}\v Clen\v en\IeC {\'\i } pr\'ace}{2}
\contentsline {chapter}{\numberline {2}SAT algoritmy}{3}
\contentsline {section}{\numberline {2.1}Teoretick\'y \'uvod}{3}
\contentsline {subsection}{\numberline {2.1.1}Booleovsk\'a formule}{3}
\contentsline {subsection}{\numberline {2.1.2}Resoluce}{4}
\contentsline {section}{\numberline {2.2}Stru\v cn\'y p\v rehled \v re\v sen\IeC {\'\i } SAT probl\'emu}{5}
\contentsline {subsection}{\numberline {2.2.1}DP algoritmus}{5}
\contentsline {subsection}{\numberline {2.2.2}DLL algoritmus}{7}
\contentsline {subsection}{\numberline {2.2.3}Binary Decision Diagrams}{9}
\contentsline {subsection}{\numberline {2.2.4}St\r almarck\r uv algoritmus}{11}
\contentsline {subsection}{\numberline {2.2.5}Stochastick\'e algoritmy}{12}
\contentsline {section}{\numberline {2.3}Sou\v casn\'e SAT solvery}{14}
\contentsline {subsection}{\numberline {2.3.1}WalkSAT}{14}
\contentsline {subsection}{\numberline {2.3.2}zChaff}{15}
\contentsline {subsubsection}{Strategie ur\v cen\IeC {\'\i } prom\v enn\'e}{15}
\contentsline {subsubsection}{BCP engine}{16}
\contentsline {subsubsection}{Anal\'yza konfliktu a u\v cen\IeC {\'\i }}{17}
\contentsline {subsubsection}{Restarty}{18}
\contentsline {subsection}{\numberline {2.3.3}EBDDRES}{19}
\contentsline {section}{\numberline {2.4}Srovn\'an\IeC {\'\i } SAT solver\r u}{20}
\contentsline {subsection}{\numberline {2.4.1}Pou\v zit\'e benchmarky}{20}
\contentsline {subsection}{\numberline {2.4.2}Porovn\'an\IeC {\'\i } heuristik WalkSATu}{21}
\contentsline {subsection}{\numberline {2.4.3}Porovn\'an\IeC {\'\i } heuristik EBDDRESu}{21}
\contentsline {subsection}{\numberline {2.4.4}V\'ysledky srovn\'an\IeC {\'\i } SAT solver\r u}{23}
\contentsline {chapter}{\numberline {3}Modifikace SAT algoritm\r u}{27}
\contentsline {section}{\numberline {3.1}Modifikace ROBDD}{27}
\contentsline {section}{\numberline {3.2}Modifikace WalkSAT algoritmu}{28}
\contentsline {section}{\numberline {3.3}Modifikace DLL algoritmu}{30}
\contentsline {section}{\numberline {3.4}DCSAT}{31}
\contentsline {subsection}{\numberline {3.4.1}Testov\'an\IeC {\'\i } DCSATu}{32}
\contentsline {chapter}{\numberline {4}Z\'av\v er}{37}
\contentsline {chapter}{Literatura}{40}
\contentsline {chapter}{\numberline {A}Manu\'al DCSATu}{41}
\contentsline {section}{\numberline {A.1}Nov\'e funkce}{41}
\contentsline {section}{\numberline {A.2}Instalace a u\v z\IeC {\'\i }v\'an\IeC {\'\i }}{42}
\contentsline {chapter}{\numberline {B}Obsah CD}{43}
