\item Explain the algorithm used to decide the equivalence of combinational circuits via the reduction to satisfiability.