Lib.rs

Circuit_SAT_Check

Simple utility to generate circuit checking to CNF formula.

Usage is simple:

./circuit_sat_check circuit1.circuit circuit2.circuit formula.cnf

The first argument is path to first circuit to compare. The second argument is path to second circuit to compare. The third argument is path to output CNF file.

Utility generates formula that unsatisfiable if circuits generates same results for all combinations of input. Otherwise formula is satisfiable.