General approach

This commit is contained in:
Théophile Bastian 2017-08-19 23:25:21 +02:00
parent c196fe0621
commit d4c10896b2
2 changed files with 54 additions and 0 deletions

View File

@ -75,3 +75,15 @@
booktitle={Int. Workshop on Designing Correct Circuits},
year={2006}
}
@article{ullmann1976algorithm,
title={An algorithm for subgraph isomorphism},
author={Ullmann, Julian R},
journal={Journal of the ACM (JACM)},
volume={23},
number={1},
pages={31--42},
year={1976},
publisher={ACM}
}

View File

@ -227,9 +227,51 @@ 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.
\todo{Mention clean codebase somewhere}
\todo{Mention VossII somewhere}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{General approach}
The global strategy used to solve efficiently the problem can be broken down to
three main parts.
\paragraph{Signatures.} The initial idea to make the computation fast is to
aggregate the inner data of a gate --- be it a leaf gate or a group --- in a
kind of hash, a 32 bits unsigned integer. This approach is directly inspired
from what was done in fl, back at Intel. This hash must be easy to compute,
and must be based only on the structure of the graph --- that is, must be
entirely oblivious of the labels given, the order in which the circuit is
described, the order in which different circuits are plugged on a wire, \ldots.
The signature equality, moreover, must be sound; that is, two signatures must
necessarily be equal if the circuits are indeed equal.
This makes it possible to rule out quickly whether two circuits are candidates
for a match or not, and run the costy actual equality algorithm on fewer gates.
\paragraph{Group equality.} The group equality algorithm is a standard
backtracking algorithm. It tries to build a match between the graphs by
trying the diverse permutations of elements with the same signature. It can
also communicate with the signing part, to request a more precise (but slightly
slower to compute) signature when it has too many permutations to try.
This part could be enhanced, but does not slow down the algorithm on the tested
examples, so I focused on other parts.
\paragraph{Pattern matching.} This part is the one responsible to answer
queries for occurrences of a sub-circuit in a circuit. It uses extensively the
signatures to determine whether two circuits could be a match or not before
spending too much time actually finding matches, but cannot rely on it as
heavily as group equality, since only the first level of precision is
applicable here (detailed later).
This part mostly consists in an implementation of Ullmann's algorithm for
subgraph isomorphism~\cite{ullmann1976algorithm}, a well-known algorithm for
this problem, that uses the specificities of the graph to be a little faster.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Signatures}
\todo{}