From d21ab27062b062308ffe7ac7f0583ee8ec2aa327 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= Date: Sat, 19 Aug 2017 18:03:20 +0200 Subject: [PATCH] A bit more text --- common/math.sty | 72 +++++++++++++++++++++++++++++++++++++++++++++++ common/refs.bib | 18 ++++++++++++ report/report.tex | 65 +++++++++++++++++++++++++++++++++++++++--- 3 files changed, 151 insertions(+), 4 deletions(-) create mode 100644 common/math.sty diff --git a/common/math.sty b/common/math.sty new file mode 100644 index 0000000..14c94b5 --- /dev/null +++ b/common/math.sty @@ -0,0 +1,72 @@ +\usepackage{stmaryrd} +\usepackage{amsmath} +\usepackage{amsfonts} +\usepackage{amssymb} +\usepackage{amsthm} +\usepackage{mathtools} +\usepackage{fancybox} + +% Intervalle discret. +\newcommand{\discrIv}[1]{\llbracket #1 \rrbracket} + +% ensembliste +\newcommand{\set}[1]{\left\{ #1 \right\}} +\newcommand{\card}[1]{\left\vert{} #1 \right\vert} +\newcommand{\abs}[1]{\left\vert{} #1 \right\vert} +\newcommand{\interior}[1]{\left({#1}\right)^\circ} +\newcommand{\floor}[1]{\left\lfloor{} #1 \right\rfloor} +\newcommand{\ceil}[1]{\left\lceil{} #1 \right\rceil} + +% Abréviations courrantes +\newcommand{\ie}{\textit{ie.}} +\newcommand{\eg}{\textit{eg.}} +\newcommand{\wrt}{\textit{wrt.}} + +% Matrices +\newcommand{\transp}{\top} + +% Notations à polices étranges +\newcommand{\domain}{\mathcal{D}} +\newcommand{\bigO}{\mathcal{O}} +\newcommand{\calA}{\mathcal{A}} +\newcommand{\calC}{\mathcal{C}} +\newcommand{\calG}{\mathcal{G}} +\newcommand{\calV}{\mathcal{V}} +\newcommand{\calT}{\mathcal{T}} +\newcommand{\calP}{\mathcal{P}} +\newcommand{\risk}{\mathcal{R}} +\newcommand{\vect}[1]{\overrightarrow{#1}} + +% Ensembles +\newcommand{\realset}{\mathbb{R}} +\newcommand{\natset}{\mathbb{N}} +\newcommand{\relset}{\mathbb{Z}} +\newcommand{\funcspace}{\mathcal{F}} + +% Probas +\newcommand{\prob}{\mathbb{P}} +\newcommand{\probP}[1]{\mathbb{P}\left(#1\right)} +\newcommand{\expec}{\mathbb{E}} +\newcommand{\expecP}[1]{\mathbb{E}\left[#1\right]} +\newcommand{\variance}{\mathbb{V}} +\newcommand{\ber}{\mathcal{B}er} +\newcommand{\bin}{\mathcal{B}in} +\newcommand{\poi}{\mathcal{P}oi} + +% Suppression des points +\newcommand{\ibar}{\overline{\imath}} +\newcommand{\jbar}{\overline{\jmath}} + +% Fonctions +%\newcommand{\functiondef}[4]{\left\lbrace \begin{tabular}{r l} #1 & \rightarrow #2 \\ #3 & \mapsto #4\end{tabular} \right.} +\newcommand{\functiondef}[4]{\begin{cases} +#1 & \to #2 \\ +#3 & \mapsto #4 +\end{cases}} + +\newcommand{\argmin}{\operatorname{argmin}} + + +% Preuve par équivalence - puces +\newcommand{\impliesbullet}{\ovalbox{$\implies$}} +\newcommand{\impliedbybullet}{\ovalbox{$\impliedby$}} diff --git a/common/refs.bib b/common/refs.bib index d013305..4af23ce 100644 --- a/common/refs.bib +++ b/common/refs.bib @@ -24,3 +24,21 @@ organization={IEEE} } +@inproceedings{babai2016graph, + title={Graph isomorphism in quasipolynomial time}, + author={Babai, L{\'a}szl{\'o}}, + booktitle={Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing}, + pages={684--697}, + year={2016}, + organization={ACM} +} + +@inproceedings{cook1971complexity, + title={The complexity of theorem-proving procedures}, + author={Cook, Stephen A}, + booktitle={Proceedings of the third annual ACM symposium on Theory of computing}, + pages={151--158}, + year={1971}, + organization={ACM} +} + diff --git a/report/report.tex b/report/report.tex index 185b29c..2949520 100644 --- a/report/report.tex +++ b/report/report.tex @@ -18,6 +18,7 @@ \usepackage{my_listings} \usepackage{my_hyperref} \usepackage{../common/internship} +\usepackage{../common/math} \bibliography{../common/refs} @@ -95,9 +96,11 @@ functions for this task. \todo{Rename this section} +\subsection{Circuit description} + \begin{figure}[!h] \begin{align*} - \textbf{Integer constant } n, m, \ldots \qquad& \\ + \textbf{Integer constant } n, m, p, q, \ldots \qquad& \\ \\ \textbf{Wire } in0, out0, ctl0, \ldots \qquad& \\ \\ @@ -109,9 +112,9 @@ functions for this task. &\textit{(three-state gate)} \\ \vert~&\text{comb} (\evec{in0}{n}, \evec{out0}{m}, \evec{e}{m}) &\textit{(combinatorial gate)} \\ - \vert~&\text{assert} (\evec{in0}{n}, \evec{e}{m)} + \vert~&\text{assert} (\evec{in0}{n}, \evec{e}{m}) &\textit{(assertion gate)} \\ - \vert~&\text{group} (\evec{c}{n}) + \vert~&\text{group} (\evec{in0}{n}, \evec{out0}{m}, \evec{c}{p}) &\textit{(circuit hierarchical group)} \\ \\ \textbf{Binary operator } \otimes ::=~ @@ -147,10 +150,64 @@ functions for this task. \caption{AST of circuits used}\label{fig:ast} \end{figure} +The circuits on which \emph{isomatch} is working are described, and internally +represented, by the AST in Figure~\ref{fig:ast}. + +The most important thing in the description of circuits here, is that those +circuits are organized as a hierarchy of \emph{circuit groups}. This hierarchy +can be seen as the construction of a circuit by assembling smaller integrated +circuits (ICs), themselves built the same way, etc. A group is composed of +sub-circuits, input pins and output pins. Each level can of course contain +``leaf'' gates, like \textit{and} or \textit{delay} gates. This is important, +because it allows the program to work on smaller areas the circuit (\eg{} +loading in memory only a part of the circuit, etc.). + +\subsection{Sought efficiency} + +The goal of \textit{isomatch} is to be applied to large circuits on-the-fly, +during their conception. Those circuits can (and will probably) be as large as +a full processor, and the software will be operated by a human, working on +their circuit. Thus, \textit{isomatch} must be as fast as possible, since +matching operation will be executed often, and often multiple times in a row. +It must then remain fast enough for the human not to lose too much time, and +eventually lose patience. + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{General approach} -\todo{} +More precisely, the problems that \emph{isomatch} must solve are the following. + +\begin{enumerate} + \item\label{prob:equal} Given two circuit groups, are they structurally + equivalent? That is, are they the same circuit, arranged in a different + way, with possibly different names, etc.? + + \item\label{prob:match} Given two circuits, \emph{needle} and + \emph{haystack}, find every (non-overlapping) occurrence of \emph{needle} in + \emph{haystack}. An occurrence is a set $S$ of sub-circuits of + \emph{haystack} such that there is a one-to-one mapping of structurally + equivalent circuits of $S$ with circuits of \emph{needle}, and those + circuits are connected the same way in both circuits. +\end{enumerate} + +Both problems are hard. The first one is an instance of graph isomorphism, as +the actual question is whether there exists a one-to-one mapping between +sub-circuits of the two groups, such that every mapped circuit is equal to the +other (either directly if it is a leaf gate, or recursively with the same +procedure); and whether this mapping respects connections (edges) between those +circuits. Graph isomorphism is known to be in NP (given a permutation of the +first graph, it is polynomial to check whether the first is equal to the second +\wrt{} the permutation), but not known to be in either P or NP-complete. Thus, +since Babai's work on graph isomorphism~\cite{babai2016graph} is only of +theoretical interest, the known algorithms remain in worst-case exponential +time, and require ad-hoc heuristics for specific kind of graphs to get maximum +efficiency. + +The second one is an instance of subgraph isomorphism problem, which is known +to be NP-complete~\cite{cook1971complexity}. Even though a few algorithms +(discussed later) are known to be efficient in most cases for this problem, it +is nevertheless necessary to implement them the right way, and with the right +heuristics, to get the desired efficiency for the given problem. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Signatures}