Daniela Ritirc, Armin Biere, Manuel Kauers,
"A Practical Polynomial Calculus for Arithmetic Circuit Verification"
: Proc. 3rd Intl. Workshop on Satisfiability Checking and Symbolic Computation (SC2'18), CEUR-WS, 7-2018
Original Titel:
A Practical Polynomial Calculus for Arithmetic Circuit Verification
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 3rd Intl. Workshop on Satisfiability Checking and Symbolic Computation (SC2'18)
Original Kurzfassung:
Generating and automatically checking proofs independently increases con?dence in the results of automated reasoning tools. The use of computer algebra is an essential ingredient in recent substantial improvements to scale veri?cation of arithmetic gate-level circuits, such as multipliers, to large bit-widths. There is also a large body of work on theoretical aspects of propositional algebraic proof systems in the proof complexity community starting with the seminal paper introducing the polynomial calculus. We show that the polynomial calculus provides a frame-work to de?ne a practical algebraic calculus (PAC) proof format to capture low-level algebraic proofs needed in scalable gate-level veri?cation of arithmetic circuits. We apply these techniques to generate proofs obtained as by-product of verifying gate-level multipliers using state-of-the-art techniques. Our experiments show that these proofs can be checked e?ciently with independent tools.
Forschungs-