Couples de buffers de même orientation

On définit une variable $x \in \mbox{I\hspace{-.15em}N}$, qui est la capacité attribuée à $b$ pour tracer ce graphe. $\Delta$ sert ici à représenter les variables de décision.

1. initialisations : tracer les contraintes de buffer vide de $b^{\prime}$;
2. $x \leftarrow 1$;
3. tracer les contraintes de buffer plein de $b$;
4. tant qu'il y a des circuits dans la trace d'exécution : ajuster $x$ comme décrit dans la section buffer plein/buffer vide;
5. retracer les contraintes de buffer plein de $b$;
6. fin de tant que;
7. $C(b, b^{\prime}) = (\Delta(b)\geq x)\wedge(\Delta(b^{\prime})\geq 1)$.

On peut remarquer que cet algorithme travaille sur deux ensembles d'arcs, un ensemble fixé par des contraintes de buffer vide, et un ensemble dont le contenu dépend de la capacité d'un buffer (conjecturée par la variable $x$). Il incrémente la valeur de $x$, pour modifier l'ensemble « variable » d'arcs, jusqu'à ce qu'il n'y ait plus de circuits.