Algorithmic Conversion of a Propisitional Proof to a "3-coloring" of a graph.

Question

https://www.youtube.com/watch?v=5ovdoxnfFVc&t=1273s as mentioned in the video above at 17:42, Every (propisitional) mathmatical statement can be converted to a graph (that satisfies a 3 coloring if true). However, the video later states that a algorithrim by cook-levin, can also use a proof to make a hypotheical coloring. I have had a hard time locating where in the papers such a process, and i need a clear place to start.