Revisiting DRUP-based Interpolants with CaDiCaL 2.0

TL;DR

This paper introduces an implementation of DRUP-based interpolants in CaDiCaL 2.0, demonstrating improved performance in model checking tasks and providing a publicly available tool for the formal methods community.

Contribution

It presents a novel integration of DRUP-based interpolant generation into CaDiCaL 2.0 using its new proof tracer API, enhancing model checking workflows.

Findings

Improved runtime performance in model checking benchmarks.

Higher number of solved instances compared to Glucose-based solver.

Implementation is publicly available and adaptable for future CaDiCaL versions.

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.