Method for speeding up boolean satisfiability
US9685959B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Sep 11, 2015 |
| Grant date | Jun 20, 2017 |
| Priority date | — |
| Expiry date | Sep 11, 2035 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06N5/013
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method for transforming a tautology check of an original logic circuit into a contradiction check of the original logic circuit and vice versa comprises interpreting the original logic circuit in terms of AND, OR, MAJ, MIN, XOR, XNOR, INV original logic operators; transforming the original circuit obtained from the interpreting, into a dual logic circuit enabled for a checking of contradiction in place of tautology and vice versa, by providing a set of switching rules configured to switch each respective one of the original logic operators INV, AND, OR, MAJ, XOR, XNOR, MIN into a respective switched logic operator INV, OR, AND, MAJ, XNOR, XOR, MIN; and complementing outputs of the original circuit by adding an INV at each output wire. The method further provides testing in parallel the satisfiability of the original logic circuit, and the satisfiability of the dual logic circuit with inverted outputs. Responsive to one of the parallel tests finishing, the other parallel test is caused to also stop.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.