Abstract
A miter encodes an equivalence check of two Boolean
circuits. This is encoded as a combinatorial problem searching
for an input for these circuits such that their output is different.
Fig 1 shows an illustration of a miter: Two circuits have the
same inputs and there is an exclusive-OR (XOR) for each
output of the circuits. If the output of one of these XORs
can be assigned to true, a certificate is found that shows that
the circuits are not equivalent. Miters are generally used as
follows: one of the two circuits is an optimized variant of
the other one. If the miter has no solution (unsatisfiable), it
means that the circuits are equivalent and that the optimization
is valid.
| Original language | English |
|---|---|
| Title of host publication | In Proceedings of SAT Competition 2013 |
| Editors | A. Balint, A. Belov, M. Heule, M. Järvisalo |
| Place of Publication | University of Helsinki |
| Publisher | Department of Computer Science |
| Pages | 104 |
| Number of pages | 1 |
| Volume | B-2013-1 |
| Publication status | Published - 2013 |
Fields of science
- 102011 Formal languages
- 102 Computer Sciences
- 101 Mathematics
JKU Focus areas
- Computation in Informatics and Mathematics