Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher.
Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?
Some links on this page may take you to nonfederal websites. Their policies may differ from this site.

Bolchini, Cristiana ; Verbauwhede, Ingrid ; Vatajelu, Ioana (Ed.)Algebraic reasoning has proven to be one of the most effective approaches for verifying gatelevel integer multipliers, but it struggles with certain components, necessitating the complementary use of SAT solvers. For this reason validation certificates require proofs in two different formats. Approaches to unify the certificates are not scalable, meaning that the validation results can only be trusted up to the correctness of compositional reasoning. We show in this paper that using dual variables in the algebraic encoding, together with a novel tail substitution and carry rewriting method, removes the need for SAT solvers in the verification flow and yields a single, uniform proof certificate.more » « less

Ivrii, Alexander ; Strichman, Ofer (Ed.)Systems mixing Boolean logic and arithmetic have been a longstanding challenge for verification tools such as SATbased bitvector solvers. Though SAT solvers can be highly efficient for Boolean reasoning, they scale poorly once multiplication is involved. Algebraic methods using Gröbner basis reduction have recently been used to efficiently verify multiplier circuits in isolation, but generally do not perform well on problems involving bitlevel reasoning. We propose that pseudoBoolean solvers equipped with cutting planes reasoning have the potential to combine the complementary strengths of the existing SAT and algebraic approaches while avoiding their weaknesses. Theoretically, we show that there are optimallength cutting planes proofs for a large class of bitlevel properties of some well known multiplier circuits. This scaling is significantly better than the smallest proofs known for SAT and, in some instances, for algebraic methods. We also show that cutting planes reasoning can extract bitlevel consequences of wordlevel equations in exponentially fewer steps than methods based on Gröbner bases. Experimentally, we demonstrate that pseudoBoolean solvers can verify the wordlevel equivalence of adderbased multiplier architectures, as well as commutativity of bitvector multiplication, in times comparable to the best algebraic methods. We then go further than previous approaches and also verify these properties at the bitlevel. Finally, we find examples of simple nonlinear bitvector inequalities that are intractable for current bitvector and SAT solvers but easy for pseudoBoolean solvers.more » « less

We show that is hard to find regular or even ordered (also known as DavisPutnam) Resolution proofs, extending the breakthrough result for general Resolution from Atserias and Muller to these restricted forms. Namely, regular and ordered Resolution are automatable if and only if P = NP. Specifically, for a CNF formula F the problem of distinguishing between the existence of a polynomialsize ordered Resolution refutation of F and an at least exponentialsize general Resolution proof being required to refute F is NPcomplete.more » « less

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 n^{O(1)} size regular resolution proofs for arbitrary degree 2 identities on array, diagonal, and Booth multipliers and n^{O(log n)} size proofs for these identities on Wallace tree multipliers.more » « less