Implement Tools for Circuit-SAT - Githubissues

cannontwo / cannon

Lifetime repository

https://cannontwo.com/cannon/

MIT License

0 stars 0 forks source link

Implement Tools for Circuit-SAT #77

Closed cannontwo closed 3 years ago

cannontwo commented 3 years ago

Should implement Circuit-SAT using existing logic stuff, so that a built circuit can be converted to CNF and then checked for satisfiability using DPLL.

More precisely, implement the following components:

[x] NAND gate (use Tseytin tranformation https://en.wikipedia.org/wiki/Circuit_satisfiability_problem#The_Tseytin_transformation)
[x] OR gate
[x] AND gate
[x] XOR gate
[x] Full Adder (with composition to make multi-digit adders) https://en.wikipedia.org/wiki/Adder_(electronics)

Implement NAND gate first, other gates in terms of NAND gates.

cannontwo commented 3 years ago

Resolved by a675d408e68cdb8b833275831a69a86415856da4