Cílem této kapitoly bude teoretický rozbor problému detekce tautologie a přiblížení základních funkčních principů algoritmů na tuto detekci, které používá minimalizační nástroj Espresso. Nakonec bude představen návrh pro vlastní implementaci jejíž realizace bude popsána v kapitole~\ref{realizace}.

\section{Volba implementačního prostředí}
\label{volbaProstredi}

Jedním z požadavků na navrhovaný systém bylo, aby byl implementován v programovacím jazyce C++. Proto se jako nejvíce vyhovující vývojové prostředí jevilo MS Visual Studio 2005, které je pro potřeby výuky volně ke stažení ze serveru~\cite{eAcademy}. Jako další alternativa pro volbu vývojového prostředí se nabízela freewareová aplikace Dev-C++, která však na první pohled nenabízí tak intuitivní uživatelské rozhraní a {\it debuggovací}\footnote{Možnosti pro ladění programu.} možnosti. Proto bylo pro vývoj zvoleno právě MS Visual Studio. Každé z těchto dvou zmiňovaných vývojových prostředí obsahuje vlastní překladač, bude proto velmi zajívamé vzájemné srovnání těchto různých kompilací stejného projektu. Tomuto porovnání výpočetních časů se budeme věnovat v podkapitole~\ref{srovnaniDevMS}.

\section{Problém tautologie}

Zodpovězení otázky, zda-li je daná logická funkce tautologií, je jedna ze základních operací využívaná v algoritmech na minimalizaci logických funkcích. Např. nástroj Espresso, který bude představen v následující podkapitole~\ref{espresso}, využívá metodu na detekci tautologie jako základ mnoha svých algoritmů\footnote{např. $IRREDUNDANT\_COVER, REDUCE, ESSENTIAL\_PRIMES, LAST\_GASP$}. Asi největší význam má detekce tautologie v metodě na určování přímých implikantů, kde je třeba ověřit, zda-li daný term je celý obsažen v původní funkci. A toto ověření se používá pro minimalizaci logických funkcí.

\clearpage
Tautologii, lze definovat jako vlastnost logické funkce. Logická funkce je tautologií, právě tehdy a jen tehdy pokud nabývá pravdivé hodnoty při jakémkoliv ohodnocení vstupních proměnných. Příkladem takovéto funkce může být:
 $$Y = a + \overline{a},$$
hodnota $Y$ bude vždy jedna nezávisle na ohodnocení proměnné $a$ z množiny $\{0, 1\}$.

Obecně je detekce tautologie problém třídy $co-NP$ (viz podkapitola~\ref{slozitost}). Pro zodpovězení této otázky bychom museli \uv{hrubou silou} ověřit všech $2^{n}$ možných ohodnocení $n$ vstupních proměnných a pro každé z nich říct, zda-li je zadaná funkce při tomto ohodnocení pravdivá či nikoli. Pokud by se nám podařilo najít jedno ohodnocení, při kterém by funkce vracela nepravdivou hodnotu, nemuseli bychom již dále pokračovat a mohli bychom o dané funkci prohlásit, že není tautologií. Máme-li funkci zadanou ve formě DNF (viz podkapitola~\ref{logFce}), a to bude náš případ, neboť vstupní formát PLA (viz podkapitola~\ref{pla}) obsahuje na každém řádku jeden součinový term, můžeme využít následující vlastnost, že pokud najdeme jeden term, který je pro dané ohodnocení splněný, je splněna celá funkce. Pro detekci tautologie lze využít mnoho dalších pravidel vyplývajících z vlastností DNF a využít je pro zefektivnění práce výpočetního algoritmu. Návrhem takovéhoto postupu se bude zabývat podkapitola~\ref{algEspresso}.

\section{Úvod do Espressa}
\label{espresso} 

Tato podkapitola se bude snažit přiblížit funkci a význam nástroje Espresso resp. Espresso-II~\cite{espresso}. Popis vychází z práce kolegy Miklánka~\cite{miklanek}, který se zabýval vytvořením knihovny z tohoto nástroje.

Program Espresso je heuristický nástroj pro dvouúrovňovou minimalizaci logických funkcí. Jeho autorem je Richard Rudell působící na University of California Berkeley v Kalifornii. Tento nástroj je široce používán - výjimkou není ani Katedra počítačů Fakulty elektrotechnické ČVUT v Praze.

Hlavní přínos Espressa spočívá v použití nových\footnote{upravovaná verze programu byla z roku 1988-1989} algoritmů, které zrychlují a obecně optimalizují heuristickou minimalizaci. Další výhodou je, že formát vstupních a výstupních souborů je kompatibilní se standardním formátem pro fyzický popis PLA\footnote{PLA - Programmable logic array}.

Espresso má nicméně i své nevýhody. Mezi největší patří použití příkazové řádky, která je podle současných standardů považována za uživatelsky nepřátelskou a dále chybí možnost použít Espresso jako modul, který by byl využíván nějakým komplexnějším programem. Pro jeho pokrokové metody se Espresso vyplatí modernizovat, rozšířit tak jeho pole působnosti a prodloužit tím dobu používání.

Této úpravě nestojí v cestě ani licence, podle které se Espresso může volně šířit a upravovat pod podmínkou zachování copyrightu\footnote{Copyright 
\copyright 1988, 1989, Regents of the University of California. All rights reserved.}.

\section{Rozbor algoritmů z Espressa}
\label{algEspresso}

V dokumentaci k minimalizačnímu nástroji Espresso-II~\cite{espresso} je popsána kostra algoritmu na detekci tautologie, která bude základem naší vlastní implementace (viz podkapitola~\ref{pozadavky}). V následujících odstavcích se budeme tomuto algoritmu věnovat.

\subsection{Základní rekurzivní schéma}
\label{zakladniSchema}

Celá detekce je založena na rekurzivním opakování základního schématu, kde se využivají obecné vlastnosti DNF a logických funkcí (viz podkapitola~\ref{logFce}). Tuto rekurzivní kostru můžeme pro zjednodušení popsat následujícím pseudokódem:

\clearpage
\begin{verbatim}
  boolean TAUTOLOGY(cover F) {                                                          
    T := SPECIAL_CASES()                // testování speciálních případů
    
    if(T == -1) UNATE_REDUCTION ()      // volání unátní redukce
    if(T == -1) COMPONENT_REDUCTION ()  // detekce komponent
 
    if(T != -1) return T                  
 
    j := BINATE_SELECT ()               // výběr nejvíce binátní proměnné
    if(0 == TAUTOLOGY(cofactor(j)) {    // musíme hledat dále v rekurzi
      return 0                          // není-li splněn, nejde o tautologii
    }     
    if(0 == TAUTOLOGY(neg_cofactor(j)){ // totéž pro neg. kofaktor
      return 0
    }  
    return 1                            // pokrytí této úrovně je tautologie
  }


    //         SPECIAL_CASES               |   VÝSLEDEK   |  NÁVRAT
    // ----------------------------------------------------------------
    // 1) řádek samých DC                  |  tautologie  |    1
    // 2) sloupec samých 0 nebo 1          |  není taut.  |    0
    // 3) nedostatečný počet uzlů          |  není taut.  |    0
    // 4) méně jak 7 vstupů -> hrubá síla  |     ---      |    ?
    // 5) nic z předchozích                |   rekurze    |   -1
\end{verbatim}

Vstupní data přicházejí ve formě PLA\footnote{Viz kapitola~\ref{pla}.} struktury. Pro jednoduchost si lze představit, že algoritmus pracuje s dvourozměrným polem, kde řádky představují jednotlivé termy a toto pole má tolik sloupců, kolik je vstupních proměnných. Používáme tři symboly: "0", "1" a "2", kde "1" značí danou proměnnou v daném termu, "0" její negaci a "2" zastupuje DC. Příklad reprezentace zadané logické funkce a jejich kofaktorů\footnote{Viz kapitola~\ref{kofaktor}.} je symbolicky znázorněn na obrázku~\ref{schema}.

Z výše uvedeného pseudokódu, který popisuje základní rekurzivní schéma našeho algoritmu je patrné, že nejprve dochází k testování daného pokrytí\footnote{Z angl. slova {\it cover}, viz reprezentace logické funkce na obr.~\ref{schema}.} na sérii speciálních případů viz výše uvedený pseudokód rekurzivního schématu. Rozlišujeme čtyři základní případy:

\begin{enumerate}
\item
{\bf řádek samých DC:} obsahuje-li dané pokrytí řádek, kde se vyskytují pouze DC symboly resp. "2" viz obr.~\ref{schema}. Je toto pokrytí tautologické, neboť jak vyplývá z definice DNF\footnote{Viz podkapitola~\ref{logFce}} stačí najít jeden term (tento řádek), který bude splněn vždy (a to tento term bude, jsou zde pouze DC), aby byla logická funkce tautologií,

\item
{\bf sloupec samých "0" nebo "1":} obsahuje-li dané pokrytí sloupec, ve kterém se vyskytují pouze symboly "1" resp. "0", pak tato funkce není tautologií, neboť se v ní daná proměnná (příslušna tomuto sloupci) vyskytuje buď v přímé resp. negované formě. Abychom našli ohodnocení, pro které funkce vrátí nepravdivou hodnotu, stačí tuto proměnnou ohodnotit jak \uv{nepravdu} resp. \uv{pravdu},

\item
{\bf nedostatečný počet uzlů:} jako spodní hranici pro minimální počet mintermů\footnote{Viz podkapitola~\ref{logFce}.} můžeme stanovit hodnotu, kterou získáme jako součet, do kterého každý term přispěje $2^{k}$, kde $k$ je rovno počtu DC v dané řádce tohoto termu. Je-li tato suma menší než $2^{n}$, kde $n$ představuje počet proměnných pak daná funkce nemůže být tautologií,

\item
{\bf méně jak 7 vstupů:} má-li testované pokrytí méně jak 7 vstupů, použije se na detekci tautologie tzv. \uv{hrubá síla}, která představuje rekurzivní funkci, která projde celou pravdivostní tabulku a zodpoví otázku, zda-li je testovaná funkce tautologie. Volání hrubé síly, je zde přípustné, neboť pravdivostní tabulka má pro 6 vstupů $2^{6} = 64$ řádků, které se dají otestovat ve velmi krátkém čase. Hranici "7" lze chápat jako parametr a v kapitole~\ref{odKdyHrubaSila}, kde se budeme zabývat testováním, zkusíme měnit tuto hodnotu a sledovat vliv na výsledný čas potřebný k nalezení řešení,

\item
{\bf nic z předešlých případů:} v daném pokrytí se nevyskytuje žádný ze speciálních případů, je třeba pokračovat dále podle schématu.
 
\end{enumerate}

\begin{figure}[h]
\begin{center}
\includegraphics[width=14cm]{obr/schema3.PNG}
\caption{Ukázka rekurzivní detekce tautologie}
\label{schema}
\end{center}
\end{figure}

Dostali jsme se nyní do stavu, kdy jsme otestovali naši funkci na sérii speciálních případů. Dále předpokládejme, že prozatím nebudeme uvažovat funkce na zefektivnění činnosti algoritmu nazvané $UNATE\_REDUCTION$ a $COMPONENT\_REDUCTION$, kterým se budeme věnovat v podkapitole~\ref{unatniRed} resp.~\ref{redukceKomp}. Jako další krok následuje výběr tzv. nejvíce binátní proměnné a jejímu výběru se věnuje podkapitola~\ref{kofaktor} a obrázek~\ref{kofaktorObr}. Heuristický výběr nejvíce binátní proměnné je velmi důležitý pro konstrukci kofaktoru\footnote{Viz podkapitola~\ref{kofaktor}.} z dané funkce. Pro efektivní práci algoritmu je vhodné, abychom dokázali detekovat sloupce unátní\footnote{Viz podkapitola~\ref{unatniRed}.}, proto je výhodné se \uv{zbavovat} sloupců binátních a v našem případě toho nejvíce binátního.

Z vybrané nejvíce binátní proměnné se vytvoří dva kofaktory: přímý a negovaný a nad každým z těchto kofaktorů se zavolá opět ta samá rekurzivní detekce tautologie, popsaná výše ovedeným pseudokódem. Původní funkci pak můžeme prohlásit za tautologii právě tehdy a jen tehdy, pokud je otázka tautologie zodpovězena kladně pro obě větve vzniklých kofaktorů.

Tento rekurzivní postup lze názorně sledovat na obrázku~\ref{schema}, kde je nejprve za nejvíce binátní proměnnou zvoleno $x_{1}$. Negovaný kofaktor vpravo můžeme ihned prohlásit za tautologii, neboť obsahuje řádek samých DC (případ 1). Levý kofaktor se dále rozdělí na dva podle proměnné $x_{2}$ atd. Na obrázku~\ref{schema} je pro každý kofaktor vyznačeno, který speciální případ u něho nastal. Je patrné, že původní funkce není tautologie, protože tautologií nebyly všechny z ní rekurzivně vzniklé kofaktory. Stejnou odpověď jsme mohli získat, ale v mnohem kratším čase, rozpoznáním toho, že proměnné $x_{2}$ a $x_{3}$ jsou unátní. Tato skutečnost je na obrázku~\ref{schema} znázorněna přerušovanou čarou v horní části. Tomuto zefektivnění se bude věnovat podkapitola~\ref{unatniRed}.

\subsection{Kofaktor, nejvíce binátní proměnná}
\label{kofaktor}

Řekli jsme, že náš nástroj na detekci tautologie obdrží na vstupu logickou funkci popsanou pomocí PLA\footnote{Viz kapitola~\ref{pla}} struktury. Tuto logickou funkci lze pak reprezentovat dvourozměrným polem, kde řádky představují jednotlivé termy a toto pole má tolik sloupců kolik je vstupních proměnných. Používáme pak tři symboly: "0", "1" a "2", kde "1" značí danou proměnnou v daném termu, "0" její negaci a "2" zastupuje DC. Kofaktor dané funkce, který je formalně definován v podkapitole~\ref{kofaktorDef}, pak hledáme vzhledem k zvolené proměnné a to buď k její přímé nebo negované formě. Abychom získali kofaktor původní funkce z přímé formy její jedné proměnné, přiřadíme do kofaktoru ty řádky, které obsahují v sloupci příslušejícímu dané proměnné "1" nebo "2" a jako hodnotu v kopírovaném řádku příslušející sloupci dané proměnné dosadíme "2". Pro negovaný kofaktor pak analogicky ty řádky, kde se nacházejí v daném sloupci "0" nebo "2". Vše lze ilustrovat obrázkem~\ref{kofaktorObr}, kde je znázorněna konstrukce přímého kofaktoru proměnné "B".

Heuristická otázka volby proměnné, ze které budeme vytvářet kofaktor, je vyřešena pomocí detekce tzv. nejvíce binátní proměnné. Tato detekce bude velmi často využívána, viz podkapitola~\ref{zakladniSchema}. Nejvíce binátní proměnnou lze definovat jako tu, která má největší počet zpárovatelných dvojic "0" a "1" v daném sloupci ze všech. Tuto detekci lze popsat následujícím pseudokódem:


\begin{verbatim}
  begin
    maxDvojic01 = 0;
    nejviceBinatniPromenna = 0;
    for ( i = 0; i < pocetPromennych; i++){	
      if(min(pocet0veSloupci[i], pocet1veSloupci[i]) > maxDvojic01){
        maxDvojic01 = min(pocet0veSloupci[i], pocet1veSloupci[i]);
        nejviceBinatniPromenna = i;
      }
    }
    return nejviceBinatniPromenna;
  end
\end{verbatim}

\begin{figure}[h]
\begin{center}
\includegraphics[width=10cm]{obr/kofaktor.PNG}
\caption{Ukázka vzniku kofaktoru z nejvíce binátní proměnné}
\label{kofaktorObr}
\end{center}
\end{figure}

\subsection{Unátní redukce}
\label{unatniRed}

Unátní redukce je jedním ze způsobů, jak zvýšit efektivitu algoritmu na detekci tautologie. Na obrázku~\ref{schema} jsme si ukázali, že rozpoznání unátních sloupců, může vést k velmi rychlému nalezení výsledku. Nyní ukážeme, v čem unátní redukce spočívá.

Základem unátní redukce je \uv{odhalení} unatních sloupců. Sloupec je unátní pokud odsahuje pouze symboly "0" a "2" nebo "1" a "2" (viz obrázek~\ref{schema}) nebo první dva sloupce na obrázku~\ref{unatniObr}. Pokud zadaná logická funkce neobsahuje žádný unátní sloupec, žádná akce se v unátní redukci nevykonává. V případě, že jsou detekovány unátní sloupce vychází se z teorému, který lze popsat pomocí obrázku~\ref{unatniObr}. 

Logickou funkci $F$ lze rozdělit do čtyř částí $\{A_{1}, X_{1}, T_{1}, F_{1}\}$ přičemž blok $A_{1}$ není tautologie a blok $T_{1}$ obsahuje pouze samé symboly "2". Lze tvrdit, že funkce $F$ je tautologie právě tehdy a jen tehdy, pokud blok $F_{1}$ je tautologie. Tento postup je základem unátní redukce, která pak probíhá následujícím způsobem. Z unátních sloupců překopírujeme ty termy, které na pozicích unátních sloupců obsahují pouze symboly "2". Neexistuje-li, žádný takovýto řádek, daná funkce není tautologie.

\begin{figure}[h]
\begin{center}
\includegraphics[width=10cm]{obr/unatniRedukce.PNG}
\caption{Schéma unátní redukce}
\label{unatniObr}
\end{center}
\end{figure}

\clearpage
\subsection{Redukce komponent}
\label{redukceKomp}

Redukce komponent je další způsob jak zvýšit efektivitu algoritmu na detekci tautologie a je založen na obdobném principu jako unátní redukce popisovaná v předchozí podkapitole~\ref{unatniRed}. Nyní ukážeme v čem redukce komponent spočívá.

Základem redukce komponent, je detekce bloků v pokrytí zadané funkce, které budeme nazývat komponentami. Předpokládejme, že se nám podaří najít řádkovou a sloupcovou permutaci v původní matici tak, že se nám tuto matici podaří upravit na tvar, který vystihuje obrázek~\ref{komponentyObr}. Danou funkci pak můžeme rozložit na bloky - komponenty $F^{1}...F^{k}$, zbytek matice je vyplněn pouze symboly "2". Poté testujeme na tautologii pouze jednotlivé komponenty, protože původní logická funkce je tautologií, pokud alespoň jedna z komponent je tautologie. Tato skutečnost může mít za následek radikální změnšení prostoru, který musíme procházet při detekci tautologie.


\begin{figure}[h]
\begin{center}
\includegraphics[width=5cm]{obr/redukceKomp.PNG}
\caption{Schéma redukce komponent}
\label{komponentyObr}
\end{center}
\end{figure}


\section{Návrh implementace}
\label{navrhImplementace}

Shrneme-li nyní požadavky\footnote{Viz podkapitola~\ref{pozadavky}.} na navrhovaný nástroj na detekci tautologie, závěr z rešeršního zpracování\footnote{Viz podkapitola~\ref{zaverReserse}.} a analýzu algoritmů z Espressa\footnote{Viz podkapitola~\ref{algEspresso}.}, dostaneme následující návrh implementace, jejíž realizací se bude zabývat kapitola~\ref{realizace}.

Základem celého nástroje na detekci tautologie bude jedna třída, která bude nést informace o datech reprezentujících logickou funkci, bude definovat metody potřebné pro detekci tautologie a bude uchovávat pomocné datové struktury potřebné pro zefektivnění práce algoritmu. Pro komunikaci s jádrem programu BOOM~II se bude využívat interface, definující dvě metody:
\begin{itemize}
\item
  bool isPlaTautology(PLA* pla); 
\item
  bool isSoPlaTautology(SoPLA* pla);
\end{itemize}

První z nich se bude používat pro práci s PLA strukturou, která je reprezentována vnitřní třídou nástroje BOOM~II. Druhá metoda je určena pro práci se strukturou SoPLA, která je speciálním případem jedno-výstupového\footnote{SoPLA = Single Output PLA}. Schéma těchto tříd je znázorněno na zjednodušeném UML diagramu popisujícím třídy jádra programu BOOM~II na obrázku~\ref{tridyBoom}. 

Úkolem realizace bude: 
\begin{itemize}

\item najít nejvýhodnější způsob pro vnitřní reprezentaci dané logické funkce s ohledem na paměťovou náročnost a s možností časově efektivního náhodného přístupu k datům na základě adresace konkrétní proměnné v konkrétním termu,

\item časově efektivní detekce speciálních případů,  

\item vytváření kofaktorů z nejvíce binátní proměnné,

\item časově efektivní detekce unátních sloupců a následná tvorba unátního derivátu podle schématu na obrázku~\ref{unatniObr},

\item vytvoření zcela vlastního efektivního algoritmu na detekci komponent a jejich následná tvorba podle schématu na obrázku~\ref{komponentyObr}.
\end{itemize}




