- run
$ python BC-CNF/testwriteadder32.py
to generate32Adder.bc
- run
$ python BC-CNF/testwriteKSA32.py
to generate 'KSA32.bc' - generate cnf file using bc2cnf tools, one of them available here
- identify the 2 output ids you want to compare, add the line
d1 id2 0 -id1 -id2 0
at the bottom of the generated cnf file - run in a SAT Solver and it should give UNSAT as the answer
Our SATSolver