Adds constraints to the dual rail formula that enforce a bijection between models of the dual rail formula and prime implicants of the original formula:
- the input atom of each witness circuit is equal to the inverse of the corresponding input when is switch is on, and to the input otherwise.
- the positive dual-rail literal of the witness circuit must be false (by adding a unit clause).
Linear Supertypes
Serializable, Serializable, Product, Equals, AnyRef, Any
Adds constraints to the dual rail formula that enforce a bijection between models of the dual rail formula and prime implicants of the original formula: - the input atom of each witness circuit is equal to the inverse of the corresponding input when is switch is on, and to the input otherwise. - the positive dual-rail literal of the witness circuit must be false (by adding a unit clause).