Questionnaire-2024/equivalence_checking/0000_sol.tex

Let $C_1$ and $C_2$ denote the two combinational circuits.
In order to check whether $C_1$ and $C_2$ are equivalent, one has to perform the following steps:
\begin{enumerate}
    \item Encode $C_1$ and $C_2$ into two propositional formulas $\varphi_1$ and $\varphi_2$.
    \item Compute the Conjunctive Normal Form (CNF) of $\varphi_1 \oplus \varphi_2$,
    using Tseitin encoding; i.e., $CNF(\varphi_1 \oplus \varphi_2)$. 
    \item Give the formula  $CNF(\varphi_1 \oplus \varphi_2)$ to a SAT solver and check for satisfiability.
    \item $C_1$ and $C_2$ are equivalent if and only if $CNF(\varphi_1 \oplus \varphi_2)$ is UNSAT.
\end{enumerate}