Cílem této kapitoly bude popis průběhu implementace nástroje na detekci tautologie, který je cílem této diplomové práce. Realizace je založena na návrhu implementace vycházejícího z analýzy uvedené v předchozí kapitole~\ref{analyza}.

\section{Průběh implementace}

Vývoj celého projektu probíhal ve třech základních fázích. V první z nich došlo k vytvoření základní funkční kostry algoritmu, který pracoval podle schématu vyjádřeného pseudokódem v podkapitole~\ref{zakladniSchema}. Tento nástroj byl schopen detekovat tautologii ze zadaných PLA struktur na vstupu, avšak výsledný čas detekce nebyl optimální. Ve většině případů byly časy potřebné pro nalezení řešení horší v porovnání s knihovnou z nástroje Espresso, která je popsaná v podkapitole~\ref{knihovnaEspresso}, a která je hlavním srovnávacím prvkem pro efektivitu našeho projektu.

Jako další krok vývoje následovala druhá fáze, která si kladla za cíl zvýšit výkonnost algoritmu, tak aby řešení bylo nalezeno v co nejkratším čase. Za tímto účelem byly do hlavní třídy přidány pomocné dynamické datové struktury, umožňujících efektivnější indexování prvků a uchování informací o jednotlivých termech a proměnných. Při vzniku odvozených pokrytí (kofaktor, unátní derivát, komponenta) - viz obrázek~\ref{schema} se inicializují informace o jednotlivých řádcích a sloupcích takto vzniklých derivátů a tyto informace se pak využívají např. pro vyhodnocování speciálních případů - viz podkapitola~\ref{zakladniSchema}. Dále došlo k optimalizaci cyklických procházení datových polí především pomocí přidání ukončovacích podmínek. Tyto úpravy vedly k požadovanému zvýšení výkonu a náš nástroj byl již téměř ve všech případech rychlejší, než knihovna z nástroje na minimalizaci logických funkcí, Espressa, což byl náš původní záměr. Následné testování však ukázalo, že existuje možnost, jak náš projekt zrychlit mnohem více a to zhruba pětinásobně. Tento efekt by měl být umožněn přechodem na výhodnější vnitřní reprezentaci zadané logické funkce a to díky rychlejšímu náhodnému přístupu ke zpracovávaným datům. 

O začátku vývoje se pro vnitřní reprezentaci dat používala třída PLA z jádra programu BOOM~II. Při testech na časovou optimálnost náhodného přístupu k datům, se ukázalo, že mnohem výhodnějším způsobem, než je zde používaný STL\footnote{Standard Template Library - standardní knihovna šablon jazyka C++} systém generických kolekcí, je přímý přístup k paměti. Poslední, třetí, fáze vývoje projektu tedy měla za cíl implementovat nový systém vnitřní reprezentace dat pomocí dynamických dvourozměrných polí. Výsledným efektem pak bylo, že nová verze nástroje na detekci tautologie přinesla několikanásobné zrychlení, které je kvantifikováno v podkapitole~\ref{srovnaniReprezentaci}.

\section{Popis realizace se zaměřením na nestandardní části řešení}
\label{nestandardniCasti}

Následující podkapitoly se budou zabývat konkrétním způsobem realizace těch částí nástroje na detekci tautologie, které jsme vymezili v části~\ref{navrhImplementace}.

\subsection{Vnitřní reprezentace logické funkce}
\label{vnitrniReprezentace}

Na samotném začátku implementace tohoto projektu se jako nejvýhodnější jevilo použít pro vnitřní reprezentaci dat představujících logickou funkci právě objektovou strukturu definovanou v jádru programu BOOM~II - třídu PLA. Tato struktura využívá třídy představující jednotivé termy ({\it class Term}) a v třídě PLA jsou pak data uložena jako typované kolekce jednotlivých termů. Pro efektivní přístup k jednotlivým řádkům (termům) je zde zavedena i podpora jejich indexování a lze i adresovat jednotlivé proměnné pro daný term. Tato struktura tedy umožňuje sekvenční procházení pokrytí dané funkce, což je důležitým předpokladem pro samotnou realizaci jednotlivých částí\footnote{Viz podkapitola~\ref{zakladniSchema}.} algoritmu na detekci tautologie.

Použitím vnitřní třídy PLA programu BOOM~II se podařilo implementovat nástroj na detekci tautologie, který poskytoval řešení ve velmi krátkých časem ve srovnání s jinými implementacemi\footnote{Viz podkapitola~\ref{resersniZpracovani}.}. Dokonce se dařilo, řešit i relativně velké instance vstupních logických funkcí, které nebyly ostatními nástroji detekovatelné (hledání řešení trvalo např. více než 200s). Během testování se však zjistilo, že by mohla existovat cesta k dalšímu zrychlení chodu algoritmu a to pomocí přechodu na alternativní reprezentaci pokrytí dané logické funkce. Toto zjištění bylo umožněno na základě srovnání časů sekvenčního průchodu dvou stejně velkých dat logických funkcí. V prvním případě se jednalo o již použitou třídu PLA (nabízí se dvě možnosti průchodu termů - pomocí iterátoru, nebo pomocí indexu), v druhém případě pak šlo o dynamické dvourozměrné pole. Tyto průchody a adresace jednotlivých prvků pro tyto tři případy jsou vyjádřeny následujícími kódy:

\begin{verbatim}
  // průchod PLA pomocí iterátoru
    PLA* pla;    
    list<Term>::iterator ti;
    TermList *data = pla->GetData();
    for ( ti = data->begin(); ti != data->end(); ti++ ){
      for(int j=0; j< numberOfVariables; j++){
        (*ti).GetIM(j);
      }
    }

  // průchod PLA pomocí indexů
    for(int i=0; i< numberOfTerms; i++){
      for(int j=0; j< numberOfVariables; j++){
        pla->GetTerm(i)->GetIM(j);
      }
    }

  // průchod dynamického 2D pole
    char **cover;
    for(int i=0; i < numberOfTerms; i++){
      for(int j=0; j < numberOfVariables; j++){
        cover[i][j];
      }
    }
\end{verbatim}

Měření bylo prováděno na procesoru AMD Athlon XP-M 2800+ 2,12GHz, 512MB RAM s operačním systémem Windows XP SP3. Výsledkem tohoto testu bylo, že poslední způsob trval u reprezentace logické funkce o velikosti 5MB (např. funkce o 1000 proměnných a 5000 termech) asi 0,01s, při procházení termů pomocí iterátoru asi 0,09s a při přístupu k termům pomocí indexů asi 0,26s. Použít průchod termy pomocí iterátoru je možné pouze v případě, že musíme projít všchny termy a tato situace nenastává vždy. I tak je zřejmé, že použití dvourozměrného dynamického pole pro reprezentaci dané logické funkce je téměř o jeden řád rychlejší než průchod pomocí iterátoru a zhruba 30x rychlejší než přistupování k termům pomocí indexů.

Na základě tohoto zjištění se vytvořila nová verze nástroje na detekci tautologie využívající pro vnitřní reprezentaci logické funkce dynamické pole. Zrychlení, které tato změna způsobila bylo natolik významné, že se rozhodlo o přepracování jádra programu BOOM~II, kde se místo nyní používaných generických kolekcí z knihovny STL začne využívat také přímý přístup do paměti. Zrychlení nástroje pomocí této úpravy je kvantifikováno v podkapitole~\ref{srovnaniReprezentaci}.

Po aplikaci těchto změn do jádra programu BOOM~II bude opět moci být využívána původní verze našeho nástroje na detekci tautologie, protože struktura PLA, se kterou pracuje, již bude využívat onu efektivnější reprezentaci dat. 

\subsection{Detekce speciálních případů}
\label{realSpecPripady}

V první funkční verzi našeho nástroje na detetci tautologie se pro detekci speciálních případů\footnote{Viz podkapitola~\ref{zakladniSchema}.} používalo sekvenční procházení pokrytí analyzované funkce. I když tyto detekční cykly obsahovaly podmínky na předčasné ukončování při nalezení nebo vyvrácení daného kritéria, byl tento způsob detekce speciálních případů velmi neefektivní. Došlo tedy k zavedení dynamických struktur, které nesou informace a jednotlivých řádcích a sloupcích testovaného pokrytí. Pro vyhodnocení všech speciálních případů je zapotřebí informace o počtu "0" a "1" v každém sloupci a počtu "2" v každém řádku. K rozhodnutí, zda-li nastává některý speciální případ, pak stačí v nejhorším případě jeden průchod těmito daty a ne již průchod celým dvourozměrným polem.

Při detekci třetího speciálního případu dochází k zajímavému problému: dosáhne-li počet proměnných více jak 3000, tak hodnota $2^{3000}$, kterou je potřeba porovnávat se součtem $2^k$, kde $k$ je počet DC v každém termu, začne jít mimo rozsah i toho největšího datového typu C++ ({\it long double} - rozsah do $10^{999}$). Pro zachování univerzálnosti našeho nástroje, bylo nutné vymyslet způsob jak porovnávat takto velká čísla a tím bylo použití bitového pole o délce počtu proměnných, kde každý bit přísluší mocnice čísla 2 dané pořadím tohoto bitu. Sčítání přes všechny řádky hodnot $2^k$, kde $k$ je počet DC v každém termu, poté probíhá tak, že se program pokusí uložit hodnotu "1" na pozici $k$, pokud je obsazená, vynuluje ji a propaguje přenos do řádu $k+1$ atd. dokud nenalezne bit z hodnotou "0". Na konci stačí porovnat maximální dosažený řád v tomto poli s hodnotou počtu proměnných.

Pro vyhodnocení čtvrtého případu, kdy nastává situace, že dané pokrytí má již méně jak sedm proměnných, bylo třeba implementovat algoritmus na detekci tautologie tzv. \uv{hrubou silou}. Tato realizace je založena na rekurzivním algoritmu generujícím postupně všechny možné konfigurace ohodnocení jednotlivých proměnných a jejich následným testováním na výslednou hodnotu dané funkce. Rekurze se zastaví pokud nalezne ohodnocení, pro které ja daná funkce {\it nepravda}, nenajde-li takové, označí pokrytí za tautologii.

\subsection{Tvorba kofaktorů z nejvíce binátní proměnné}
\label{realKofaktor}

Pro vytvoření kofaktoru je nezbytné určit proměnnou podle, které budeme její dva kofaktory (v přímé a negované formě) vytvářet. Proč je výhodné, aby touto proměnnou byla právě ta, kterou nazýváme \uv{nejvíce binátní} popisuje podkapitola~\ref{zakladniSchema}. A detekcí nejvíce binátní proměnné a tvorbou kofaktoru se zabývá podkapitola~\ref{kofaktor}.

Jak je vidět z pseudokódu na detekci nejvíce binátní proměnné v podkapitole~\ref{kofaktor}, využívají se zde také stejné struktury popisující dané sloupce jako v případě detekce speciálních případů. Díky těmto informacím o počtu "0" a "1" v jednotlivých sloupcích je určení nejvíce binátní proměnné možné jedním průchodem pole o délce rovné počtu proměnných. Bez této pomocné struktury bychom musel projít celým pokrytím.

Máme-li nyní určenou nejvíce binátní proměnnou, je třeba vytvořit dva kofaktory - viz schéma na obrázku~\ref{kofaktorObr}. Nejprve je třeba určit nové rozměry pokrytí představující vzniklý kofaktor. To provedeme spočítáním termů, které budou obsaženy v novém kofaktoru a uložením indexů těchto řádků. Počet sloupců (počet proměnných) poté bude vždy o jedna měnší, nemá cenu již dále uvažovat s původně nejvíce binátním sloupcem, který by měl v kofaktoru podobu samých "2".

Po určení rozměrů pokrytí kofaktoru alokujeme potřebnou pamět a inicializujeme pomocné dynamické datové struktury podle rozměrů daného kofaktoru. Poté naplníme kofaktor daty, viz obrázek~\ref{kofaktorObr}, za pomoci uložených indexů kopírovaných termů. V tomto případě nelze použít rychlejší přístup k termům pomocí iterátoru\footnote{Viz podkapitola~\ref{vnitrniReprezentace}.}, protože neprocházíme postupně všechny termy a jsme tedy odkázáni pouze na přístup k termům pomocí indexů. Při tomto plnění dat kofaktoru současně detekujeme hodnoty jednotlivých symbolů a aktualizujeme informace v pomocných strukturách popisujích jednotlivé řádky a sloupce.

Nad takto vzniklými dvěma kofaktory se poté rekurzivně spustí stejná analýza jako na původní pokrytí, ze kterého tyto kofaktory vznikly - viz pseudokód základního schématu v podkapitole~\ref{zakladniSchema}. Heuristickou otázkou by nyní mohlo být: nad kterým kofaktorem (větví rekurze), spustit detekci dříve? Nabízí se řešení vyplývající z třetího specialního případu, který může prohlásit dané pokrytí za netautologické pokud obsahuje nedostatečný počet DC symbolů. Proto budeme volat nejprve vyhodnocení kofaktoru s nižším počtem DC, abychom urychlili případnou detekci netautologií, protože v případě, že se o tautologii jedná, musí se projít obě rekurzivní větve.


\subsection{Realizace unátní redukce}

Pro efektivní využití přínosu, který nám nabízí unátní redukce, jejíž princip je popsán v podkapitole~\ref{unatniRed}, je třeba v co možno nejkratším čase rozpoznat přítomnost unátních sloupců. Při této detekci se opět uplatní struktura nesoucí informace o jednotlivých sloupcích. Unátní sloupce rozpoznáme jedním průchodem tímto polem o délce rovné počtu proměnných, protože unátní sloupec je takový, který neobsahuje žádné symboly "0" resp. "1" a přitom obsahuje alespoň jednu hodnotu "1" resp. "0".

V případě, že pokrytí neobsahuje žádné unátní sloupce, žádná další akce se v tomto bodě nekoná a toto zjištění nás nestálo příliš mnoho času. V druhém případě, když jsme detekovali unátní sloupce, vede toto zjištění k velmi významnému zmenšení prostoru, který musíme dále procházet a testovat na tautologii. Z původního pokrytí vytvoříme unátní derivát podle schématu na obrázku~\ref{unatniObr}. Nejprve zjistíme rozměry nového pokrytí, které vznikne po unátní redukci a přitom si ukládáme indexy těch řádků (obsahujících pouze "2" na pozicích unátních proměnných) a sloupců (unátní sloupce), které se stanou součástí unátního derivátu.

Po určení rozměru nového pokrytí a vymezení rozsahu dat, který se budou dále používat, alokujeme potřebné datové struktury a naplníme je daty obdobně jako při vzniku kofaktoru - viz podkapitola~\ref{realKofaktor}.

Nad takto vzniklým unátním derivátem se poté rekurzivně spustí stejná analýza jako na původní pokrytí, ze kterého vznikl - viz pseudokód základního schématu v podkapitole~\ref{zakladniSchema}. 

\subsection{Detekce a tvorba komponent}
\label{realKomponenty}

Princip a využití detekce komponent je popsán v podkapitole~\ref{redukceKomp}. Naším úkolem bude nyní vymyslet zcela vlastní algoritmus, který bude schopen tyto komponenty detekovat a vytvářet.

Detekci komponent založíme na faktu, že každý řádek může příslušet maximálně jedné komponentě. Vyjdeme-li na počátku od libovolného řádku a budeme-li prohledávat celou oblast pokrytí a detekovat rozsah komponenty příslušející tomuto řádku dostaneme na závěr tohoto postupu dvě možná řešení. Buď bude nalezená komponenta shodná s původním pokrytím a v tomto případě již nelze toto pokrytí dělit na menší komponenty a žádné urychlení běhu detekce tautologie nás nečeká a nebo v druhém případě nalezneme komponentu vymezenou mřížkou danou protnutím se konkrétních řádků a sloupců. V tomto druhém případě jsme z původního pokrytí vybrali některé řádky, které náleží menší komponentě, než je původní pokrytí a tento postup detekce komponent můžeme zopakovat, když začneme hledat od libovolného dalšího řádku, který ještě nebyl použit pro žádnou z komponent. Tento postup opakujeme do té doby, než všechny řádky z původního pokrytí budou příslušet nalezeným komponentám. Je tedy jedno, od kterého řádku jsme na počátku začali deketci odvíjet.

Která data však spadají do jedné komponenty? Je třeba od počátečního řádku procházet všechny sloupce, které v tomto řádku neobsahují symbol "2" a v těchto sloupcích je třeba uložit na zásobník unikátní indexy těch řádků, které obsahují symboly "0" nebo "1" tzv. incidují v ortogonálních směrech s výchozím řádkem. Ukládáme indexy takto \uv{proscanovaných} sloupců. Poté tento postup opakujeme pro další řádek podle indexu z vrcholu zásobníku a \uv{scanujeme} ty sloupce, které dosud nebyly kontrolovány.

Tento postup lze sledovat na obrázku~\ref{schemaRedKomp}, kde v prvním případě máme dva ekvivalentní způsoby zápisu jednoho pokrytí logické funkce. Tyto dvě matice lze mezi sebou převést pomocí záměny příslušných řádků a sloupců, což jsme zde udělali pouze pro názornost, aby v druhém případě byly na první pohled vidět dvě komponenty, které lze získat z původního pokrytí. Pro funkci algoritmu na detekci komponent nemá zaměňování řádků a sloupců žádný vliv. V první fázi vyznačené na obrázku~\ref{schemaRedKomp} modrou číslicí jedna dojde k určení startovacího řádku, ve kterém budeme \uv{scanovat} všechny sloupce, které neobsahují v tomto řádku DC symbol (znázorněn pomocí "-"). Při procházení těchto sloupců (na obr. fáze 2) přidáváme na zásobník unikátní indexy těch řádků, které v tomto procházeném sloupci neobsahují DC symboly (obsahují "0" nebo "1") a zároveň si uložíme informaci, které sloupce už jsme takto \uv{proscanovali}. Ve fázi 3 opakujeme postup pro řádek z vrcholu zásobníku a procházíme dosud \uv{neproscanované} sloupce. Postup opakujeme do té doby, než je zásobník prázdný. V tuto chvíli jsme našli oblast komponenty obsahující startovací řádek a tuto komponentu máme vymezenou rozsahem indexů řádků a sloupců, které jí příslušejí. Obsahuje-li takto vymezená komponenta všechny řádky z původního pokrytí (případ $b$~na~obrázku~\ref{schemaRedKomp} - symbol~\textcolor{red}{1} způsobil propojení obou komponent z případu $a$ do jedné), nelze toto pokrytí rozdělit na menší komponenty. V opačném případě, když detekovaná komponenta obsahuje pouze některé řádky, opakujeme postup na detekci jedné komponenty pro startovací řádek, kterým muže být kterýkoliv z řádků původního pokrytí, který doposavaď nebyl zařazen do žádné jiné komponenty a to do té doby, než všechny řádky původní matice jsou přiřazeny konkrétním komponentám.


\clearpage
Po úspěšném detekování dvou a více komponent je nutné vytvořit jejich objektové reprezentace v programu pro další zpracování algoritmem na detekci tautologie.  Alokujeme potřebné datové struktury a naplníme je daty obdobně jako při vzniku kofaktoru - viz podkapitola~\ref{realKofaktor}. Účel a přínos detekce komponent je popsán v podkapitole~\ref{redukceKomp} a vyplývá z něho, že podaří-li se nám detekovat dvě a více komponent, tak původní pokrytí je tautologie právě tehdy a jen tehdy, pokud alespoň jedna z komponent je tautologie. Metoda na detekci komponent:
\begin{verbatim}
   vector<Tautology*>  Tautology::findComponents();
\end{verbatim}
vrací po úspěšné dektekci dvou a více komponent jejich seznam v podobě STL vektoru nesoucí ukazatele na jednotlivé komponenty - instance třídy {\it Tautology}, která reprezentuje dané pokrytí logické funkce a obsahuje metody a pomocné datové struktury pro detekci tautologie viz následující podkapitola~\ref{datStruktury}. Máme-li nyní k dospozici seznam komponent, stačí je postupně otestovat na tautologii stejným způsobem jako původní logickou funkci. V případě, že kterákoliv z komponent je tautologie, bylo tautologií i pokrytí, ze kterého tyto komponenty vznikly.

\begin{figure}[h]
\begin{center}
\includegraphics[width=14cm]{obr/schemaRedukceKomponent.PNG}
\caption{Detekce komponent}
\label{schemaRedKomp}
\end{center}
\end{figure}

\clearpage
Následující kód ukazuje výše popisovaný hlavní cyklus detekující rozsah jedné komponenty:
\begin{verbatim}
  vector<int> stack;
  stack.push_back(rowIndex);
  while(!stack.empty()){
    int exploringRow = stack.back();
    stack.pop_back();
    selectedRows[exploringRow] = 1;
    totalComponentedRows[exploringRow] = 1;
    selectedRowIndexes[componentRows] = exploringRow;
    componentRows++;
    for (int j = 0; j < countVariables; j++){
      if(sopla->GetTerm(exploringRow)->GetIM(j) != '-' 
         && selectedColumns[j] == -1){
        selectedColumns[j] = 1;
        selectedColumnsIndexes[componentColumns] = j;
        componentColumns++;
        for (int i = 0; i < countTerms; i++){
          if(sopla->GetTerm(i)->GetIM(j) != '-' && selectedRows[i] == -1){
            stack.push_back(i); 
            selectedRows[i] = 1;
          }
        }
      }	
    }
  }
\end{verbatim}

Nyní, když víme, jak komponenty detekovat a vytvářet, zůstává otázkou: u jakých funkcí se vyplatí tuto deketci volat, protože samotná detekce, je časově náročná, v nejhorším případě dosahuje složitosti obdobné jako sekvenční průchod celým pokrytím funkce. Komponenty lze detekovat pouze v relativně \uv{řídkých} maticích. Nastavením ideální meze, od kdy se vyplatí tuto detekci volat, se bude věnovat podkapitola~\ref{prinosUnatniAKomponent}.

\section{Popis datových struktur}
\label{datStruktury}

V podkapitole~\ref{navrhImplementace} zabývající se návrhem implementace jsme vymezili zde popisovaný nástroj na detekci tautologie jako jeden zapouzdřený celek. Ten bude rozdělen do dvou tříd: první třída {\it Cover} nese informace o datech reprezentujících logickou funkci, definuje metody potřebné pro detekci tautologie a uchovává pomocné datové struktury potřebné pro zefektivnění práce algoritmu. Druhá třída {\it TautologyDetecor} pak definuje metody pro komunikaci s okolním prostředím a realizuje detekci tautologie pomocí rekurzivního volání metody {\it tautology}, viz podkapitola~\ref{zakladniSchema}. Tato třída je rovněž integrovatelná do jádra programu BOOM~II a pro komunikaci s ním bude využívat interface definující dvě metody pro práci se strukturami $PLA$ a $SoPLA$. 

\begin{figure}[h]
\begin{center}
\includegraphics[width=14cm]{obr/tautologyClass2.PNG}
\caption{Diagram tříd TautologyDetection a Cover}
\label{classTautology}
\end{center}
\end{figure}

Schéma  tříd {\it Cover} a {\it TautologyDetector} je znázorněno pomocí class diagramu na obrázku~\ref{classTautology}. Rozdělení programu na tyto dvě třídy bylo nezbytné kvůli potřebě dealokování paměti po vyhodnocení daneho pokrytí při rekurzivním běhu programu. Hlavní třídy jádra programu BOOM~II, které jsou potřebné pro detekci tautologie a základní vztahy mezi jsou pak vyjádřeny pomocí obrázku~\ref{tridyBoom}.

\begin{figure}[h]
\begin{center}
\includegraphics[width=15cm]{obr/tridy.PNG}
\caption{Třídy jádra programu BOOM~II}
\label{tridyBoom}
\end{center}
\end{figure}

\section{Přenositelnost na jiné platformy}

Cílem tohoto projektu bylo vytvořit nástroj na detekci tautologie, který bude inegrovatelný do jádra programu na minimalizaci logických funkcí, BOOM~II, jehož zdrojové kódy nejsou vázány na konkrétní operační systém. Náš nástroj na detekci tautologie by měl tedy být rovněž platformově nezávislý a to se podařilo splnit. Jelikož byl projekt vyvíjen pod operačním systémem Windows, byl z testovacích důvodů pro účely měření doby vykonávání výpočtu použit hlavičkový soubor {\it windows.h}. Při skutečném nasazení našeho nástroje pak již tento \uv{\#include} nebude potřeba a projekt bude možné kompilovat nezávisle na druhu platformy (ověřeno pro Linux). Samotná funkce měřící čas, který výpočetní proces strávil na CPU\footnote{Central Processing Unit} je použita z webových stránek předmětu $X36PAA$~\cite{paa}.

\section{Odhad asymptotické složitosti}
\label{odhadSlozitosti}

V podkapitole~\ref{slozitost} jsme zařadili problém detekce tautologie do třídy $co-NP$. V nej\-horším možném případě nelze obecně tautologii detekovat v polynomiálním čase a jinak to tedy nebude ani s použitím našeho nástroje na detekci tautologie, který pracuje na rekurzivním principu podle schématu definovaném v podkapitole~\ref{zakladniSchema}. Budeme se tedy nyní ptát na asymptotickou složitost našeho algoritmu, tedy na počet kroků, které algoritmus bude muset vykonat, aby nalezl řešení instance problému o velikosti $N$ v tom nejméně příznivém případě, kdy nedochází k detekci speciálních případů. V rekurzivním běhu algoritmu dochází v každém cyklu k rozdělení daného pokrytí na dvě další, přičemž počet proměnných klesne o jedna (nejvíce binátní proměnná, podle které vzniknout dva kofaktory). Hloubka rekurzivního stromu je tedy $N$ a každý uzel se nám rozděluje na dvě větve. Výsledná asymptotická složitost pak vychází $2^N$, tedy stejná jakou má algoritmus deteketující tautologii pomocí \uv{hrubé síly}.

Efektivnost našeho algoritmu je však založena na detekci speciálních případů, unátní redukci a detekci komponent, které jsou popsány v podkapitole~\ref{nestandardniCasti}. Díky těmto opatřením dosahujeme mnohem vyšší výkonnosti, která je však závislá na charakteru konkrétního zadání. Výkonnost lze demostrovat v následující kapitole~\ref{testovani}, která se zabývá testováním.

Budeme-li se dále ptát na paměťovou složitost zjistíme, že v nejhorším možném případě bude program potřebovat udržet v paměti tolik reprezentací kofaktorů, jakou má maximál\-ní hloubka rekurzivního stromu a tou je $N$, kde $N$ je počet proměnných resp. $N-7$ hranice, od kdy se volá hrubá síla. Dále budeme uvažovat, že počet proměnných a termů se pro vzniklý kofaktor sníží o jedna. Pak paměťovou složitost můžeme popsat následujícím vztahem:

 $$ O(N^{2} * T). $$




