Name
Abstract | ||
|---|---|---|
We eliminate a key roadblock to efficient verification of nonlinear integer arithmetic using CDCL SAT solvers, by showing how to construct short resolution proofs for many properties of the most widely used multiplier circuits. Such short proofs were conjectured not to exist. More precisely, we give nO(1) size regular resolution proofs for arbitrary degree 2 identities on array, diagonal, and Booth multipliers and nO(log n) size proofs for these identities on Wallace tree multipliers.
|
Year | DOI | Venue |
|---|---|---|
2017 | 10.1145/3319396 | Journal of the ACM |
Keywords | DocType | Volume |
Multiplier verification,SAT solvers,resolution proofs | Conference | 66 |
Issue | ISSN | Citations |
3 | 0004-5411 | 1 |
PageRank | References | Authors |
0.36 | 19 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Paul Beame | 1 | 2234 | 176.07 |
| Vincent Liew | 2 | 7 | 1.16 |