skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


Title: Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
Systems mixing Boolean logic and arithmetic have been a long-standing challenge for verification tools such as SAT-based bit-vector 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 bit-level reasoning. We propose that pseudo-Boolean 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 optimal-length cutting planes proofs for a large class of bit-level 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 bit-level consequences of word-level equations in exponentially fewer steps than methods based on Gröbner bases. Experimentally, we demonstrate that pseudo-Boolean solvers can verify the word-level equivalence of adder-based multiplier architectures, as well as commutativity of bit-vector multiplication, in times comparable to the best algebraic methods. We then go further than previous approaches and also verify these properties at the bit-level. Finally, we find examples of simple nonlinear bit-vector inequalities that are intractable for current bit-vector and SAT solvers but easy for pseudo-Boolean solvers.  more » « less
Award ID(s):
1714593
PAR ID:
10309376
Author(s) / Creator(s):
; ; ; ;
Editor(s):
Ivrii, Alexander; Strichman, Ofer
Date Published:
Journal Name:
Proceedings of the 20th Conference on Formal Methods in Computer Aided Design, FMCAD 2020
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; (, TU Wien Academic Press)
    Narodytska, Nina; Rümmer, Philipp (Ed.)
    Clausal proofs, particularly those based on the deletion resolution asymmetric tautology (DRAT) proof system, are widely used by Boolean satisfiability solvers for expressing proofs of unsatisfiability. Their success stems from their simplicity and scalability. When solvers go beyond pure propositional reasoning, however, generating clausal proofs becomes more difficult. Solvers that employ pseudo-Boolean reasoning, including cutting-planes operations, can express proofs in the VeriPB proof system, but its adoption is not widespread. We introduce PBIP (Pseudo-Boolean Implication Proof), a framework that provides an intermediate representation between VeriPB and clausal proofs. We also introduce a toolchain comprising 1) a VeriPB-to-PBIP translator that performs proof trimming and optimization, and 2) a PBIP-to-LRAT translator that makes use of proof-generating operations on ordered binary decision diagrams (BDDs) to generate clausal proofs in LRAT format, a variant of the DRAT that allows efficient checking. We demonstrate the viability of our approach, the effectiveness of our trimming, and the performance of our clausal proof generator on a set of native PB benchmarks and compare our approach to direct checking of VeriPB proofs. 
    more » « less
  2. ; (, International Conference on Tools and Algorithms for the Construction and Analysis of Systems)
    Fisman, D.; Rosu, G. (Ed.)
    When augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has no solution. By converting the intermediate constraints generated by the PB solver into ordered binary decision diagrams (BDDs), a proof-generating, BDD-based SAT solver can then produce a clausal proof that the input formula is unsatisfiable. Working together, the two solvers can generate proofs of unsatisfiability for problems that are intractable for other proof-generating SAT solvers. The PB solver can, at times, detect that the proof can exploit modular arithmetic to give smaller BDD representations and therefore shorter proofs. 
    more » « less
  3. ; ; ; (, 2022 Design, Automation & Test in Europe Conference & Exhibition (DATE))
    Bolchini, Cristiana; Verbauwhede, Ingrid; Vatajelu, Ioana (Ed.)
    Algebraic reasoning has proven to be one of the most effective approaches for verifying gate-level 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
  4. ; (, arXiv.org)
    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
  5. ; ; ; ; ; (, ArXivorg)
    We develop a new semi-algebraic proof system called Stabbing Planes which formalizes modern branch-and-cut algorithms for integer programming and is in the style of DPLL-based modern SAT solvers. As with DPLL there is only a single rule: the current polytope can be subdivided by branching on an inequality and its “integer negation.” That is, we can (non-deterministically choose) a hyperplane ax ≥ b with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying ax ≥ b, the points satisfying ax ≤ b, and the middle slab b − 1 < ax < b. Since the middle slab contains no integer points it can be safely discarded, and the algorithm proceeds recursively on the other two branches. Each path terminates when the current polytope is empty, which is polynomial-time checkable. Among our results, we show that Stabbing Planes can efficiently simulate the Cutting Planes proof system, and is equivalent to a tree-like variant of the R(CP) system of Krajicek [54]. As well, we show that it possesses short proofs of the canonical family of systems of F_2-linear equations known as the Tseitin formulas. Finally, we prove linear lower bounds on the rank of Stabbing Planes refutations by adapting lower bounds in communication complexity and use these bounds in order to show that Stabbing Planes proofs cannot be balanced. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email