Cílem této kapitoly bude vymezení požadavků, které byly stanoveny na navrhovaný systém. Dále bude následovat rešeršní srovnání již existujících implementací a nakonec budou definovány některé základní pojmy, na které se budeme v této diplomové práci odkazovat.

\section{Vymezení cílů DP a požadavků na navrhovaný systém}
\label{pozadavky}

Byly stanoveny tyto požadavky na navrhovaný systém:
\begin{itemize}
\item 
Navrhnout a v jazyce C++ implementovat nástroj, který bude schopen vyhodnotit, zda-li je funkce na vstupu zadaná ve formě součtu součinů (DNF\footnote{Viz podkapitola~\ref{logFce}.}) tautologií.

\item 
Důraz by měl být kladen na časovou efektivitu výpočtu a uvažovat by se mělo i s možností kombinace různých algoritmů pro detekci tautologie, za účelem optima\-lizace rychlosti.

\item 
Nástroj by měl být optimalizován tak, aby efektivně pracoval s různorodými instancemi vstupních logických funkcí. Každou funkci lze charakterizovat mj. pomocí tří základních kriterií (počet vstupních proměnných, počet termů, procentuelní zastoupení DC\footnote{\uv{Don't Care stav} - na hodnotě tohoto vstupu v daném termu nezáleží.} znaků). Více se touto problematikou, různorodostí instancí, zabývá kapitola~\ref{testovani}.

\item 
Program by měl být primárně založen na algoritmech použitých v nástroji na minimalizaci logických funkcí, Espresso~\cite{espresso}.

\item 
Výsledný program by měl tvořit zapouzdřený celek, který bude možné začlenit do jádra nástroje na minimalizaci logických funkcí, BOOM~II \cite{boom}. Jako vstup bude používat struktury vlastní programu BOOM~II. Více o těchto datových strukturách se zle dočíst v podkapitole~\ref{pla}.
\end{itemize}

Cílem této diplomové práce je tedy vytvořit takto výšše specifikovaný funkční celek a otestovat jej na různých testovacích úlohách. Tyto výsledky pak budeme porovnávat s řešeními již hotových nástrojů na detekci tautologie. Tyto programy jsou blíže popsány v podkapitolách~\ref{komplement} -~\ref{grafy-popis}.



\section{Definice základních pojmů}

Následující podkapitoly si kladou za cíl přiblížit některé základní pojmy, na které se budeme v této diplomové práci odkazovat. Podrobnější definice těchto pojmů jsou pak k dispozici v uvedených zdrojových materiálech.

\subsection{Logická funkce}
\label{logFce}

Logickou funkci lze popsat následujícím způsobem~\cite{dml}:

Každé formuli o $n$ logických proměnných odpovídá pravdivostní tabulka. Na tuto tabulku se můžeme dívat jako na zobrazení, které každé $n$-tici 0 a 1 přiřazuje 0 nebo 1. Řádek pravdivostní tabulky je popsán $n$-ticí 0 a 1, hodnota je pak pravdivostní hodnota formule pro toto dosazení za logické proměnné. Zobrazení z množiny všech $n$-tic 0 a 1 do množiny \{0, 1\} se nazývá {\it Booleova funkce}. Naopak platí, že pro každou {\it Booleovu funkci} existuje formule, která této funkci odpovídá. 

{\bf Booleova funkce}. {\it Booleovou funkcí} $n$ proměnných, kde $n$ je přirozené číslo, rozumíme každé zobrazení $f:\{0, 1\}^{n} \rightarrow  \{0, 1\}$ tj. zobrazení, které každé $n$-tici $(x_{1}, x_{1},..., x_{n})$ nul a jedniček přiřazuje nulu nebo jedničku (označenou $f(x_{1}, x_{1},..., x_{n})$).

{\bf Disjunktivní normální tvar (DNF)}. Literál je logická proměnná nebo negace logické proměnné. Řekneme, že formule je v disjunktivním normálním tvaru, zkráceně v DNF, jestliže je disjunkcí jedné nebo několika formulí, z nichž každá je literálem nebo konjunkcí literálů. 
Poznamenejme, že literálu nebo konjunkci literálů se také říká minterm. Jestliže každý minterm obsahuje všechny proměnné, říkáme, že se jedná o úplnou DNF.

\subsection{Formát PLA}
\label{pla}

Jako zdroj dat pro načítání logických funkcí budou použity soubory typu PLA formátu Espresso, proto se krátce zmíníme o jejich struktuře. Pomocí PLA, lze reprezentovat logickou funkci ve formátu DNF.

Na začátku souboru se nachází klíčová slova, která popisují strukturu a vlastnosti souboru. Po nich jsou vypsány řádky se součinovými termy. Celou funkci potom dostáváme jako logický součet všech těchto řádků (termů).

{\bf Ukázkový příklad PLA}

Příklad funkce o 5 proměnných, jsou zadány jejich jména, zadáno jméno výstupní proměnné, explicitně vyjádřen počet termů a nechybí ukončení PLA.
\begin{verbatim}
    .i 5
    .o 1
    .ilb a b c d e
    .ob y
    .p 4
    10-0- 1
    -0-11 1
    00-0- 1
    -1101 1
    .e
\end{verbatim}

Výše uvedené PLA představuje funkci: $y=a\overline{bd} + \overline{b}de + \overline{abd} + bc\overline{d}e$ 

\subsection{Asymptotická složitost ve vztahu k detekci tautologie}
\label{slozitost}

Asymptotická složitost slouží jako nástroj pro porovnávání efektivity a rychlosti vykonávání jednotlivých algoritmů a definuje několik základních tříd~\cite{asympSloz} např.: $P$, $NP$, $co-NP$.

Budeme-li chtít zařadit problém detekce tautologie, do konkrétní třídy dojdeme k závěru, že spadá mezi úlohy kategorie $co-NP$, která je protějškem třídy $NP$, a to protože u~problémů třídy $NP$ dostáváme při kladné odpovědi na ověření navrhovaného řešení (tzv. {\it konfigurace}) kladnou odpověď na zadání problému (např. Je daná funkce splnitelná? - stačí při ověřování najít jedno ohodnocení vstupních proměnných-konfiguraci, při kterém je funkce splněna a získáme tím kladnou odpověď na původní otázku - ověříme certifikát). Budeme-li se ptát např. na otázku: Je daná funkce vždy splněna (je tautologií)?  - nezískáme kladným ohodnocením konfigurace certifikát. Tento problém je tedy z třídy $co-NP$.


\subsection{Kofaktor logické funkce}
\label{kofaktorDef}

Při analýze a realizaci algoritmu na detekci tautologie budeme často používat pojmu {\it kofaktor}. Nyní uvedeme jeho formální definici~\cite{logSynthesis}.

Nechť $f$ je logická funkce a $x = (x_1, x_2,..., x_n)$ jsou její proměnné, pak kofaktor $f_a$ z funkce $f$ a jejího literálu $a = x_i$ nebo $a = \overline{x_i}$ je:

 $f_{x_{i}}(x_1, x_2,..., x_n) = f(x_1,...,x_{i-1}, 1, x_{i+1},..., x_n),$
 
 $f_{\overline{x_{i}}}(x_1, x_2,..., x_n) = f(x_1,...,x_{i-1}, 0, x_{i+1},..., x_n).$

Budeme-li kofaktor $f_{C}$ vytvářet z logické funkce $f$ s ohledem k zadanému termu $C$ budou součástí vzniklého kofaktoru ty termy, které se shodují v hodnotách svých proměnných s daných termem $C$. Tento postup lze sledovat na následujícím příkladu:

 $ f = ab\overline{c} + \overline{a}b\overline{d} + abcd, $
 $ C = ab, $ 
 
 $ f_{C} = f_{ab} = \overline{c} + cd. $



\section{Rešeršní zpracování existujících implementací}
\label{resersniZpracovani}

Po vymezení požadavků na navrhovaný systém začalo testování již existujících programů na detekci tautologie, které doporučil vedoucí této práce, pan Fišer. Cílem bylo zjistit, v~jakých časech dokáží tyto programy řešit jednotlivé vstupní instance. Toto úvodní testování nebylo nijak rozsáhlé ani systematické, šlo především o získání představy, v~jakých řádech se budou pohybovat časy potřebné pro nalezení řešení. Mnohem rozsáhlejší a systematičtější testování se zaměřením na vlivy jednotlivých kritérií charakterizujících danou logickou funkci na vstupu, bude provedeno po naprogramování vlastního nástroje na detekci tautologie, který je předmětem této diplomové práce. Tomuto testování je věnována kapitola~\ref{testovani}.

Následující podkapitoly se zabývají základním popisem implementací, se kterými bude porovnáván náš program.

\section{Výpočet komplementu}
\label{komplement}

Tato implementace nástroje na detekci tautologie vznikla jako semestrální projekt kolegy Radka Chromého~\cite{chromy}. V dokumentaci tohoto projektu, je podrobně popsáno jak celý algoritmus pracuje. Hlavní myšlenka je taková, že dochází k postupnému sekvenčnímu zpracování všech termů na vstupu. Každý term se pak porovnává po znacích se všemi termy v paměti. Mohou nastat dvě situace:

\begin{enumerate}
\item term již je v paměti obsažen a je možné jej vypustit

\item term v paměti není celý obsažen, je třeba jej rozdělit na patřičný počet termů, které se pak přidají do paměti.
\end{enumerate}

Na konci výpočtu jsou v paměti termy, které tvoří dohromady komplement vstupní funkce. Je-li komplement prázdny, byla původní funkce tautologie.

Asymptotická složitost tohoto programu je exponencielní, protože algoritmus prochází při každém kroku celou paměť, tzn. N porovnání na M kroků. Paměť se sice dynamicky mění, nicméně v nejhorším případě v každém kroku se může term v paměti násobit nejhůře mohutností množiny a tato mohutnost je menší než $POCET\_PROMENNYCH$. To~znamená, že nejhorší časová složitost je pak: $$M * POCET\_PROMENNYCH * 2^{POCET\_PROMENNYCH -1}.$$

{\bf Hodnocení:}

Tento algoritmus na detekci tautologie založený na hledání komplementu zadané logické funkce najde řešení velmi rychle u malých instancí zhruba do 20 vstupních proměnných a 500 termů. S rostoucí velikostí instancí se pak čas potřebný na nalezení řešení rapidně zvyšoval. Někdy program skončil neočekávanou výjimkou. S roustoucím procentem DC znaků se rychlost programu zvyšovala.

\section{Binární rozhodovací diagramy}
\label{bdd-popis}

Tento projekt na detekci tautologie vznikl jako bakalářská práce kolegy Michala Navrkala~\cite{navrkal}. V dokumentaci této práce je podrobně popsáno, jak celý program pracuje. V následujícím odstavci připomeneme pouze základní princip.


\subsection{Definice BDD}

Pod zkratkou BDD se skrývá stromová struktura, která může být velmi vhodná pro detekci tautologie a to v případě, že se nám ji podaří \uv{uspořádat a redukovat}\footnote{Viz podkapitola~\ref{usporadaniRedukce}.}. Poté můžeme v konstantním čase detekovat, zda-li je takto reprezentovaná logická funkce tautologie, protože pokud ano, pak její graf má podobu jedničkového terminálu. 

Každá funkce je reprezentovaná jako orientovaný acyklický graf, který tvoří vnitřní uzly (neterminální uzly). Ty pak korespondují vždy s určitou proměnnou funkce, kterou dané BDD\footnote{Binary Decision Diagram, Binární rozhodovací diagram} reprezentuje. 

Graf také tvoří uzly koncové (terminální uzly, listy), které jsou označeny 1 nebo 0 a reprezentují příslušnou logickou konstantní hodnotu. Z každého neterminálu $v$ vedou dvě výstupní hrany. Jedna do tzv. low-potomka a druhá do tzv. high-potomka (dále jen low($v$) a high($v$)).

Jako příklad může posloužit obrázek~\ref{BDD}~\cite{bddWiki} ilustrující reprezentaci funkce $f$($x$1,$x$2,$x$3) definovanou pravdivostní tabulkou. Každý neterminální uzel $v$ je označen proměnnou var($v$) a má dvě hrany směřující ke dvěma potomkům :

\begin{itemize}
\item 
low($v$) označen čárkovanou čarou (případ, kdy proměnná je nulová),
\item
high($v$) označen plnou čarou (případ, kdy proměnná je jedničková).
\end{itemize}

Každý terminální uzel je označen 0 nebo 1. Pro dané přiřazení hodnot proměnných je hodnota funkce určena procházením grafu z kořene k terminálu, kde rozhodnutí o větvení je prováděno na základě hodnoty dané proměnné v přiřazení. Jako hodnotu funkce dostaneme hodnotu terminálu na konci cesty.

\begin{figure}[h]
\begin{center}
\includegraphics[width=15cm]{obr/BDD2.PNG}
\caption{Příklad BDD}
\label{BDD}
\end{center}
\end{figure}

Když už víme, jak reprezentovat logickou funkci pomocí grafu, můžeme operace nad booleovskými funkcemi implementovat jako grafové algoritmy. Ačkoli BDD representace logické funkce může mít obecně velikost exponenciálně závislou na počtu proměnných, v praxi dospějeme k mnohem kompaktnější reprezentaci.

\subsection{Uspořádání a redukce}
\label{usporadaniRedukce}

Pro snazší práci s BDD je třeba provést následující dvě operace: uspořádání a redukci. Po použití redukce získáme OBDD (ordered BDD). Aby se BDD stalo OBDD musíme vyžadovat určité uspořádání proměnných. Pro každý uzel $u$ a jeho potomka $v$ musí platit následující nerovnost:
 $$var(u) < var(v).$$

Takto popsaný OBDD má však ještě jednu nevýhodu a tou je možná redundance dat. Abychom ji odstranili, nadefinujeme tři transformační pravidla pro takovýto graf:
\begin{enumerate}
\item 
{\bf odstranění duplicitních terminálů}: eliminujeme všechny terminály se stejnou hodnotou až na jeden,
\item 
{\bf odstranění duplicitních neterminálů}: když neterminální uzly $u$ a $v$ mají var($u$)=var($v$), low($u$)=low($v$) a high($u$)=high($v$), potom jeden z uzlů $u$ a $v$ odstraníme a všechny hrany vedoucí do odstraněného uzlu převedeme do druhého uzlu,
\item 
{\bf odstranění redundantních uzlů}: když neterminální uzel $v$ má low($v$)=high($v$), potom ho odstraníme a všechny vstupní hrany převedeme do low($v$).
\end{enumerate}
Aplikací těchto pravidel na obecný OBDD dostaneme ROBDD (reduced OBDD), tedy minimalizovaný nebo-li redukovaný uspořádaný binární rozhodovací diagram.

\begin{figure}[h]
\begin{center}
\includegraphics[width=15cm]{obr/BDD3.PNG}
\caption{Použití redukčních pravidel na BDD}
\label{BDD2}
\end{center}
\end{figure}

Jak je vidět z obrázku~\ref{BDD2}~\cite{navrkal} první pravidlo zredukovalo počet terminálních uzlů z 8 na 2. Druhé pravidlo odstranilo dva uzly označené proměnnou $x$3 a nakonec třetí pravidlo odstranilo dva redundantní uzly, jejichž vstupní hrany jsme \uv{přemostili} do jednoho z potomků.

ROBDD má hned několik výhod oproti BDD, např. můžeme v konstantním čase detekovat, zda-li je takto reprezentovaná logická funkce tautologie, protože pokud ano, pak její graf má podobu jedničkového terminálu.

{\bf Hodnocení:}

Tento nástroj, rovněž jako algoritmus popisovaný v části~\ref{komplement}, poskytuje řešení v relativně rozumných časech pro malé instance. Jednu testovanou funkci z asi 30 testovaných však program označil za tautologii, i když jí nebyla. S rostoucím procentem zastoupení DC znaků výkonnost klesá.


\section{Knihovna s nástrojem Espresso}
\label{knihovnaEspresso}

Cílem bakalářské práce~\cite{miklanek} kolegy Martina Miklánka bylo vytvořit knihovnu z nástroje Espresso, který slouží k minimalizaci logických funkcích. Práce, kromě návrhu a implementace rozhraní knihovny, zahrnuje také transformaci původních zdrojových kódů z jazyka K\&R C do jazyka C++. Knihovna je použitelná pod operačními systémy Microsoft Windows a Linux, a to jak ve statické, tak i dynamické verzi.

Využijeme tedy tuto knihovnu, zapouzdřenou do vlastního spouštěcího mechanizmu k detekci tautologie.

Naše vlastní implementace nástroje na detekci tautologie, která je předmětem této DP bude též založena na algoritmech popsaných v nástroji Espresso. Bude tedy velmi důležité, porovnat rychlosti jednotlivých implementací: naše vlastní vs. knihovna z BP~\cite{miklanek} pana Miklánka, ve které se uvádí, cituji:

{\it \uv{Rozhodně se nepovedlo odhalit a opravit všechny chyby. Taková úprava by byla časově náročná, vyžádala by si značnou refaktorizaci zdrojových kódů a výsledek by dle mého názoru za to nestál. Osobně bych se přiklonil k vytvoření zcela nového projektu, který by si z původního Espressa odnesl jenom algoritmy a poučení, že by se rozhodně neměla podceňovat kontrola alokování paměti.} }


{\bf Hodnocení:}

Tato implementace dokáže řešit i větší instance než algoritmy popisované v podkapitolách~\ref{komplement} a ~\ref{bdd-popis}. Avšak pro velká vstupní PLA např. při 100 vstupních proměnných o 20000 termech již výpočetní čas začíná značně narůstat.


\section{Manipulace s logickými funkcemi pomocí grafů}
\label{grafy-popis}

Dalšími nástroji pro detekci tautologie budou dva algoritmy popsané v diplomové práci~\cite{vala} kolegy Petra Váli, který se zabýval manipulací s logickými funkcemi pomocí grafů. V dokumentaci této práce je podrobně popsáno, jak algoritmy pracují. V následujícím odstavci připomeneme pouze základní princip.

{\bf Popis algoritmu}

Algoritmus pracuje tak, že se snaží dokázat, že funkce tautologií není. Tedy hledá takové ohodnocení proměnných, které vede k tomu, že výsledek žádného z termů není jedna. Vykonává to tak, že vhodně v iteracích ohodnocuje jednotlivé proměnné tak, aby tímto krokem vždy vyřadil nějaký ze zbývajících termů coby kandidátů na splnění aktuálního ohodnocení. V počátečním stavu jsou kandidáty všechny termy. Algoritmus se vždy zaměří na některý z nich a nastaví některé z proměnných tohoto termu takovou polaritu, aby výsledkem tohoto termu již nemohla být pravda. Takto \uv{znehodnocuje} jednotlivé termy až do chvíle, kdy nezbývá žádný platný term. V takovém případě končí, neboť nenalezl ohodnocení, jehož výsledkem není pravda, nebo do chvíle, kdy zbývající kandidáty není schopen vyřadit ze seznamu kandidátů. Pak je tato větev již skutečně tautologická a v takovém případě vrací některá rozhodnutí o ohodnocení zpět (backtracking) a volí jiné způsoby, jakými proměnné ohodnocovat. Jestliže algoritmus prošel všechny větve stavového prostoru, ve kterých se mohlo nacházet řešení a nezdařilo se mu najít ohodnocení, které hledal, prohlásí funkci za tautologii.

Příklad první fáze postupu tohoto algoritmu, lze sledovat na obrázku~\ref{grafVala}~\cite{vala}, kdy se dostaneme do stavu, kdy už není způsob, jakým by se dalo zabránit splnění termu č. 5.  

\begin{figure}[h]
\begin{center}
\includegraphics[width=16cm]{obr/grafVala.PNG}
\caption{Algoritmus řešící tautologii pomocí grafů}
\label{grafVala}
\end{center}
\end{figure}

\clearpage
Druhým testovaným algoritmem pana Vály pak je algoritmus s předpřípravou PLA, která spočívá ve volání metody {\it simplification}, která efektivně zjednodušuje PLA na základě zákonu absorbce, absorbce negace a idempotence.

{\bf Hodnocení:}

Oba algoritmy z diplomové práce pana Vály nalézají řešení relativně rychle pro instance s procentuálním zastoupením DC znaků větším jak 70\%. U velkých instancí jejich výkonnost rapidně klesá. Druhý popisovaný algoritmus (s předpřípravou PLA) poskytuje řešení většinou pomaleji.


\section{Závěr rešeršního zpracování}
\label{zaverReserse}
Po otestování pěti výšše popsaných algoritmů jsem nenalezl žádný, který by byl schopen řešit velké vstupní instance\footnote{vstupní PLA větší 5MB (1000 proměnných, 5000 termů)} a přitom by byl univerzálně použitelný co do různorodosti procentuálního zastoupení DC symbolů. Našim cílem tedy bude vytvořit nástroj, který bude schopen toto splnit, bude tedy nalézat řešení v přijatelných časech i pro větší zadání, než která byla řešitelná zde srovnávanými algoritmy. 


\begin{table}[h!t]
\caption{Srovnání implementací na detekci tautologie}
\begin{center}
\begin{tabular}{|l|c|c|c|}
\hline
\bf{algoritmus}&\bf{chybovost}&\bf{velikost instance} & \bf{\% DC}\\
\hline
komplement & neošetřené výjimky & pouze pro malá PLA & více \%DC : rychlejší \\
\hline
BDD & 1 špatný výsledek & pouze pro malá PLA & více \%DC : pomalejší\\
\hline
knih. Espresso & bez chyb & i středně velká PLA & pomalé pro DC kolem 60\%\\
\hline
graf & bez chyb & i středně velká PLA & vhodné pro DC přes 70\% \\
\hline
graf2 & bez chyb & i středně velká PLA & vhodné pro DC přes 70\%\\
\hline
\end{tabular}
\end{center}
\label{tab:reserse}
\end{table}

