pith. sign in

arxiv: 1907.00087 · v2 · pith:CTK4D764new · submitted 2019-06-28 · 💻 cs.LO

DRAT-based Bit-Vector Proofs in CVC4

Alex Ozdemir , Aina Niemetz , Mathias Preiner , Yoni Zohar , Clark Barrett This is my paper

Pith reviewed 2026-05-25 12:49 UTC · model grok-4.3

classification 💻 cs.LO
keywords bit-vector proofsDRAT proofsSAT integrationSMT proof infrastructurebit-blastingproof productionproof checkingsatisfiability modulo theories
0
0 comments X

The pith

Three approaches integrate DRAT proofs from SAT solvers into an SMT solver for bit-vector formulas.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes methods for taking proofs produced by a SAT solver on a bit-blasted formula and incorporating them into the overall proof system of an SMT solver that reasons about fixed-size bit-vectors. The work presents three distinct ways to perform this integration, then measures how each affects the time to produce the final proof and the time to check it. A sympathetic reader would care because bit-vector reasoning is widely used in hardware and software verification, and machine-checkable proofs increase trust in the solver's answers. The evaluation shows that the choice of integration method creates measurable differences in these performance measures.

Core claim

The paper claims that DRAT proofs generated by an off-the-shelf SAT solver can be lifted into the proof infrastructure of an SMT solver for the theory of fixed-size bit-vectors by means of three integration approaches, and that the strengths and weaknesses of these approaches can be compared through concrete implementation and measurement of proof-production time and proof-checking time.

What carries the argument

Three integration approaches that translate DRAT proofs on the Boolean level back to proofs at the bit-vector level after bit-blasting.

If this is right

  • An SMT solver can emit machine-checkable proofs for bit-vector problems by delegating to a SAT solver that produces DRAT proofs.
  • The three integration approaches produce different performance profiles for proof generation versus proof validation.
  • Proof checking becomes feasible at the original bit-vector level rather than only at the Boolean level.
  • Off-the-shelf SAT solvers with DRAT support can be used as back-ends without losing the ability to produce end-to-end proofs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same lifting techniques could be applied to other SMT theories whose decision procedures reduce to SAT.
  • End-to-end proof pipelines become feasible for verification tasks that combine bit-vector reasoning with other theories.
  • Further engineering could focus on minimizing the size of the lifted proofs to reduce checking overhead in large instances.

Load-bearing premise

The translation step from SAT-level DRAT proofs to bit-vector-level proofs preserves soundness.

What would settle it

A concrete bit-vector formula on which the SMT solver outputs an unsatisfiability claim together with a lifted DRAT proof, yet an independent proof checker rejects the proof or a direct search finds the formula satisfiable.

Figures

Figures reproduced from arXiv: 1907.00087 by Aina Niemetz, Alex Ozdemir, Clark Barrett, Mathias Preiner, Yoni Zohar.

Figure 1
Figure 1. Figure 1: Side condition for checking a specified DRAT proof. The side conditions cnf has bottom, is rat, and cnf remove clause are defined in the same signature. Type cnfc is a constructor for CNF formulas, and is defined in a separate signature. written within them by way of the Curry-Howard correspondence. Like LF, LFSC is a framework in which axioms and derivation rules can be defined for multiple theories and t… view at source ↗
Figure 2
Figure 2. Figure 2: Derivation rules for checking that a clause constitutes an extension. Complex Side Conditions Simple Side Conditions DRAT · unit propagation · resolvent search LRAT · guided unit propagation · resolvent search ER · deferred resolution [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Side conditions across our signatures. includes a contradiction; (ii) the proof begins with an addition of a (proper or improper) RAT; or (iii) the proof begins with a deletion of some clause. In (ii) and (iii), the same side condition is recursively called on the rest of proof, with an updated working formula. In (ii), side condition is rat checks whether the added clause is indeed a RAT via resolvent sea… view at source ↗
Figure 4
Figure 4. Figure 4: Producing and checking LFSC proofs in DRAT, LRAT and ER proof systems in CVC4. White boxes are CVC4-internal components; blue boxes are external libraries. solver, and optionally produce an LRAT proof that is forwarded to the LRAT LFSC pipeline. In case of DRAT LFSC proofs, we can directly use the optimized proof and formula emitted by DRAT-trim. For ER LFSC proofs, we first use drat2er to translate the op… view at source ↗
Figure 5
Figure 5. Figure 5: Runtime distribution on 12539 commonly proved problems [PITH_FULL_IMAGE:figures/full_fig_p006_5.png] view at source ↗
read the original abstract

Many state-of-the-art Satisfiability Modulo Theories (SMT) solvers for the theory of fixed-size bit-vectors employ an approach called bit-blasting, where a given formula is translated into a Boolean satisfiability (SAT) problem and delegated to a SAT solver. Consequently, producing bit-vector proofs in an SMT solver requires incorporating SAT proofs into its proof infrastructure. In this paper, we describe three approaches for integrating DRAT proofs generated by an off-the-shelf SAT solver into the proof infrastructure of the SMT solver CVC4 and explore their strengths and weaknesses. We implemented all three approaches using cryptominisat as the SAT back-end for its bit-blasting engine and evaluated performance in terms of proof-production and proof-checking.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper describes three approaches for integrating DRAT proofs generated by an off-the-shelf SAT solver (CryptoMiniSat) into CVC4's proof infrastructure for bit-vector formulas that have been bit-blasted to SAT, explores their strengths and weaknesses, and reports an implementation and performance evaluation focused on proof-production and proof-checking times.

Significance. If the integration approaches are sound, the work enables production of verifiable proofs for bit-vector problems inside CVC4, which strengthens applications of SMT solving that require certificates. The concrete implementation using an existing DRAT-capable SAT backend and the reported runtime data on proof generation/checking provide practical evidence of feasibility and trade-offs among the methods.

major comments (2)
  1. [description of the three approaches] The manuscript provides no explicit formal argument, invariant, or machine-checked claim establishing that a DRAT refutation of the bit-blasted SAT instance entails unsatisfiability of the original bit-vector formula (the lifting step through the encoder's auxiliary variables and clauses). This is load-bearing for the central claim that the DRAT proofs can be soundly incorporated into CVC4's bit-vector proof infrastructure.
  2. [evaluation section] The evaluation reports only runtime for proof production and checking; it contains no data on proof sizes, no end-to-end validation that checked proofs correspond to the source formulas, and no comparison against a non-proof-producing baseline, which weakens the ability to assess whether the approaches deliver usable certificates.
minor comments (1)
  1. [Abstract] The abstract states that three approaches are described but does not name or briefly characterize them, reducing immediate readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments. We address each major comment below and indicate planned revisions.

read point-by-point responses

  1. Referee: The manuscript provides no explicit formal argument, invariant, or machine-checked claim establishing that a DRAT refutation of the bit-blasted SAT instance entails unsatisfiability of the original bit-vector formula (the lifting step through the encoder's auxiliary variables and clauses). This is load-bearing for the central claim that the DRAT proofs can be soundly incorporated into CVC4's bit-vector proof infrastructure.

    Authors: We agree that the manuscript does not contain an explicit formal argument or invariant for the lifting step. The three approaches assume soundness of the bit-blasting encoding and of DRAT, but this is not spelled out. In the revised version we will add a short subsection providing a high-level soundness argument, including the key invariants preserved by the encoder and how a DRAT refutation of the SAT instance entails unsatisfiability of the original bit-vector formula. revision: yes

  2. Referee: The evaluation reports only runtime for proof production and checking; it contains no data on proof sizes, no end-to-end validation that checked proofs correspond to the source formulas, and no comparison against a non-proof-producing baseline, which weakens the ability to assess whether the approaches deliver usable certificates.

    Authors: We acknowledge the evaluation section is limited to runtime figures. In the revision we will add proof-size measurements for all three approaches. We will also clarify that proof checking occurs inside CVC4's existing infrastructure and therefore validates against the original formulas; if space permits we will include a short additional experiment or discussion on this point. Finally, we will report runtimes for a non-proof-producing baseline to quantify overhead. revision: yes

Circularity Check

0 steps flagged

No circularity: implementation and evaluation paper with no derivation chain

full rationale

The paper describes three approaches for integrating DRAT proofs from an off-the-shelf SAT solver into CVC4's bit-vector proof infrastructure, implemented with cryptominisat and evaluated on proof-production and proof-checking performance. No equations, fitted parameters, predictions, or self-referential derivations appear. The work is an engineering report on implementation choices and runtime measurements; it does not claim to derive any result from first principles or reduce any quantity to itself by construction. The soundness of lifting DRAT proofs is treated as an external property of the underlying SAT and bit-blasting components rather than something established inside the paper via a load-bearing self-citation or definition.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review reveals no free parameters, axioms, or invented entities; the contribution is described as an engineering implementation of proof integration.

pith-pipeline@v0.9.0 · 5657 in / 1056 out tokens · 41177 ms · 2026-05-25T12:49:15.749521+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages

  1. [1]

    In: Proceedings of the 23rd International Con- ference on Computer Aided Verification

    Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi´ c, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Proceedings of the 23rd International Con- ference on Computer Aided Verification. pp. 171–177. CAV’11, Springer-Verlag (2011), http://dl.acm.org/citation.cfm?id=2032305.2032319

    work page arXiv 2011

  2. [2]

    In: Delahaye, D., Woltzenlogel Paleo, B

    Barrett, C., de Moura, L., Fontaine, P.: Proofs in satisfiability modulo theories. In: Delahaye, D., Woltzenlogel Paleo, B. (eds.) All about Proofs, Proofs for All, Mathematical Logic and Foundations, vol. 55, pp. 23–44. College Publications, London, UK (2015)

    work page 2015

  3. [3]

    In: Gupta, A., Kroening, D

    Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfi- ability Modulo Theories (Edinburgh, UK) (2010)

    work page 2010

  4. [4]

    In: International Conference on Automated Deduction

    Cruz-Filipe, L., Heule, M.J., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: International Conference on Automated Deduction. pp. 220–236. Springer (2017)

    work page 2017

  5. [5]

    In: Financial Cryptography Workshops

    Dickerson, T.D., Gazzillo, P., Herlihy, M., Saraph, V., Koskinen, E.: Proof-carrying smart contracts. In: Financial Cryptography Workshops. Lecture Notes in Com- puter Science, vol. 10958, pp. 325–338. Springer (2018)

    work page 2018

  6. [6]

    In: Giunchiglia, E., Tacchella, A

    E´ en, N., S¨ orensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing. pp. 502–518. Springer Berlin Heidelberg, Berlin, Heidelberg (2004)

    work page 2004

  7. [7]

    In: CAV (2)

    Ekici, B., Mebsout, A., Tinelli, C., Keller, C., Katz, G., Reynolds, A., Barrett, C.W.: Smtcoq: A plug-in for integrating SMT solvers into coq. In: CAV (2). Lecture Notes in Computer Science, vol. 10427, pp. 126–133. Springer (2017)

    work page 2017

  8. [8]

    In: Interna- tional Symposium on Artificial Intelligence and Mathematics (ISAIM)

    Gelder, A.V.: Verifying RUP proofs of propositional unsatisfiability. In: Interna- tional Symposium on Artificial Intelligence and Mathematics (ISAIM). Springer (2008)

    work page 2008

  9. [9]

    In: LPAR

    Hadarean, L., Barrett, C.W., Reynolds, A., Tinelli, C., Deters, M.: Fine grained SMT proofs for the theory of fixed-width bit-vectors. In: LPAR. Lecture Notes in Computer Science, vol. 9450, pp. 340–355. Springer (2015)

    work page 2015

  10. [10]

    Journal of the ACM 40(1), 143–184 (1993)

    Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM 40(1), 143–184 (1993)

    work page 1993

  11. [11]

    In: International Joint Conference on Automated Reasoning

    Kiesl, B., Rebola-Pardo, A., Heule, M.J.: Extended Resolution Simulates DRAT. In: International Joint Conference on Automated Reasoning. pp. 516–531. Springer (2018)

    work page 2018

  12. [12]

    In: POPL

    Necula, G.C.: Proof-carrying code. In: POPL. pp. 106–119. ACM Press (1997)

    work page 1997

  13. [13]

    In: Berre, D.L., J¨ arvisalo, M

    Pardo, A.R., Biere, A.: Two flavors of drat. In: Berre, D.L., J¨ arvisalo, M. (eds.) Proceedings of Pragmatics of SAT 2015 and 2018. EPiC Series in Computing, vol. 59, pp. 94–110. EasyChair (2019)

    work page 2015

  14. [14]

    Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic prob- lems. In: SAT. Lecture Notes in Computer Science, vol. 5584, pp. 244–257. Springer (2009)

    work page 2009

  15. [15]

    Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Form. Methods Syst. Des. 42(1), 91–118 (2013)

    work page 2013

  16. [16]

    development team, T.C.: The coq proof assistant reference manual version 8.9 (2019), https://coq.inria.fr/distrib/current/refman/

    work page 2019

  17. [17]

    Tseitin, G.S.: On the Complexity of Derivation in Propositional Calculus, pp. 466–

    work page

  18. [18]

    Springer Berlin Heidelberg, Berlin, Heidelberg (1983)

    work page 1983

  19. [19]

    In: Sinz, C., Egly, U

    Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: Efficient Checking and Trim- ming Using Expressive Clausal Proofs. In: Sinz, C., Egly, U. (eds.) Theory and Ap- plications of Satisfiability Testing – SAT 2014. pp. 422–429. Springer International Publishing, Cham (2014)

    work page 2014