Couples de buffers de sens opposés

La variable $x \in \mbox{I\hspace{-.15em}N}$ est la capacité conjecturée de $b$, et la variable $y \in \mbox{I\hspace{-.15em}N}$ la capacité conjecturée de $b^{\prime}$.

1. initialisations : $y \leftarrow 1$ et $C(b, b^{\prime}) \leftarrow \emptyset$;
2. répéter : tracer les contraintes de buffer plein de $b^{\prime}$, et utiliser l'algorithme précédent pour trouver une valeur de $x$ nous permettant de tracer un graphe sans circuits;
3. $C(b, b^{\prime}) \leftarrow C(b, b^{\prime}) \vee ((\Delta(b)\geq x)\wedge(\Delta(b^{\prime})\geq y))$;
4. $y \leftarrow y+1$
5. jusqu'à $x = 1$;

Cet algorithme teste pour chaque capacité du buffer $b$, la capacité à attribuer à $b^{\prime}$ et les consigne dans une expression logique à satisfaire.