Revisiting DRUP-Based Interpolants with CaDiCaL 2.0

Abstract

Abstract We present our implementation of DRUP-based interpolants in 2.0, and evaluate performance in the bit-level model checker using the Hardware Model Checking Competition benchmarks. is a state-of-the-art, open-source SAT solver known for its efficiency and flexibility. In its latest release, version 2.0, 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 , we enable its use in model-checking workflows that require interpolants. Our experimental evaluation shows that integrating with DRUP-based interpolants in results in better performance (both runtime and number of solved instances) when compared to with 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 . Since our implementation uses the API, it should be maintainable and applicable to future releases of .