Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Revisiting DRUP-based Interpolants with CaDiCaL 2.0

Basel Khouri, Yakir Vizel

TL;DR

This work implements DRUP-based interpolants inside CaDiCaL 2.0 by leveraging its Tracer API to maintain a separate DRUP proof and perform on-the-fly interpolant construction. The Drup2Itp framework decouples interpolation from solver internals, enabling proof core extraction, minimization, and replay-driven interpolant generation, including an incremental Minimizer variant. Experimental results in Avy on HWMCC benchmarks show that CaDiCaL with Drup2Itp improves runtime and solved-instance counts compared to Glucose-based configurations, and can even solve instances that were previously unsolved within a one-hour limit. The implementation is public and designed to be extendable to other proof formats, offering a flexible path to stronger interpolation-driven model checking with modern SAT solvers.

Abstract

We present our implementation of DRUP-based interpolants in CaDiCaL 2.0, and evaluate performance in the bit-level model checker Avy using the Hardware Model Checking Competition benchmarks. CaDiCaL is a state-of-the-art, open-source SAT solver known for its efficiency and flexibility. In its latest release, version 2.0, CaDiCaL introduces a new proof tracer API. This paper presents a tool that leverages this API to implement the DRUP-based algorithm for generating interpolants. By integrating this algorithm into CaDiCaL, we enable its use in model-checking workflows that require interpolants. Our experimental evaluation shows that integrating CaDiCaL with DRUP-based interpolants in Avy results in better performance (both runtime and number of solved instances) when compared to Avy with Glucose as the main SAT solver. Our implementation is publicly available and can be used by the formal methods community to further develop interpolation-based algorithms using the state-of-the-art SAT solver CaDiCaL. Since our implementation uses the Tracer API, it should be maintainable and applicable to future releases of CaDiCaL.

Revisiting DRUP-based Interpolants with CaDiCaL 2.0

TL;DR

This work implements DRUP-based interpolants inside CaDiCaL 2.0 by leveraging its Tracer API to maintain a separate DRUP proof and perform on-the-fly interpolant construction. The Drup2Itp framework decouples interpolation from solver internals, enabling proof core extraction, minimization, and replay-driven interpolant generation, including an incremental Minimizer variant. Experimental results in Avy on HWMCC benchmarks show that CaDiCaL with Drup2Itp improves runtime and solved-instance counts compared to Glucose-based configurations, and can even solve instances that were previously unsolved within a one-hour limit. The implementation is public and designed to be extendable to other proof formats, offering a flexible path to stronger interpolation-driven model checking with modern SAT solvers.

Abstract

We present our implementation of DRUP-based interpolants in CaDiCaL 2.0, and evaluate performance in the bit-level model checker Avy using the Hardware Model Checking Competition benchmarks. CaDiCaL is a state-of-the-art, open-source SAT solver known for its efficiency and flexibility. In its latest release, version 2.0, CaDiCaL introduces a new proof tracer API. This paper presents a tool that leverages this API to implement the DRUP-based algorithm for generating interpolants. By integrating this algorithm into CaDiCaL, we enable its use in model-checking workflows that require interpolants. Our experimental evaluation shows that integrating CaDiCaL with DRUP-based interpolants in Avy results in better performance (both runtime and number of solved instances) when compared to Avy with Glucose as the main SAT solver. Our implementation is publicly available and can be used by the formal methods community to further develop interpolation-based algorithms using the state-of-the-art SAT solver CaDiCaL. Since our implementation uses the Tracer API, it should be maintainable and applicable to future releases of CaDiCaL.
Paper Structure (24 sections, 1 theorem, 3 equations, 6 figures, 1 table, 3 algorithms)

This paper contains 24 sections, 1 theorem, 3 equations, 6 figures, 1 table, 3 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. CNF, Resolution, and UP
  5. Validating Clausal Proofs
  6. Interpolation and Colors
  7. Craig Interpolant
  8. Sequence Interpolant
  9. The Model Checker Avy
  10. Implementing DRUP-based Interpolants in CaDiCaL
  11. The Drup2Itp class
  12. Generating Interpolants On-The-Fly
  13. Initialization
  14. Solving
  15. Trimming The Proof
  16. ...and 9 more sections

Key Result

lemma thmcounterlemma

Given a CNF formula $G$ and a clause $c$, $c$ is deducible from $G$ by UP iff $c$ is deducible from $G$ by trivial resolution. That is, $G\vdash_{\textsc{UP}} c \iff G\vdash_{\textsc{TVR}} c$.

Figures (6)

  • Figure 1: The Drup2Itp class
  • Figure 2: Clause object.
  • Figure 3: Proof iterator
  • Figure 4: Comparing performance with and without Minimizer.
  • Figure 5: Proof size comparison while disabling pre-/in-processing during minimization.
  • ...and 1 more figures

Theorems & Definitions (3)

  • definition thmcounterdefinition: RUP
  • lemma thmcounterlemma: 21
  • definition thmcounterdefinition: $N$-Colored CNF