{"id":"67c2c234-c38c-42cf-98d3-e56f921066c4","arxiv_id":"2501.02608","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"A new DRUP-based interpolation framework for CaDiCaL 2.0, integrated into Avy, outperforms the Glucose-based baseline on HWMCC'19 and HWMCC'20 benchmarks.","lead":"This paper presents Drup2Itp, a tool that extracts DRUP proofs from the CaDiCaL SAT solver via its new Tracer API and turns them into interpolants for model checking. It reports that wiring this into the Avy model checker improves runtime and solved instances over the standard Glucose-based version on hardware model checking benchmarks.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The paper's performance claim rests on an unverified DRAT-as-DRUP assumption: if CaDiCaL 2.1.2 ever emits a RAT clause, Drup2Itp's RUP-based replay can yield unsound interpolants, invalidating the Avy comparison.","rationale":"The reader's weakest assumption already names the absence of explicit interpolant validation, and the paper itself flags the DRAT-as-DRUP issue as a caveat. I judge this to be the most load-bearing because it is a correctness precondition: if the proofs are not DRUP, the core algorithm in §3.2–3.3 is not even applicable, and the empirical numbers in Table 1 lose their meaning. The alternative concern—that the abstract overstates the result since the plain CaDiCaL row solves fewer instances than Glucose on HWMCC'19 (203 vs. 205)—is real but secondary; the Minimizer row does outperform Glucose on both benchmark families, so the claim can be repaired by scoping it to the Minimizer configuration. The DRAT-as-DRUP issue cannot be repaired by rephrasing; it requires evidence. I agree with the reader's identification of missing correctness validation, so I mark agreement. The CONDITIONAL verdict remains appropriate: the implementation and benchmark study are useful and reproducible, but the paper must either verify the DRUP assumption (e.g., by showing that all learned clauses pass RUP) or provide an independent interpolant validity check before the performance claim should be accepted.","tokens_in":14540,"tokens_out":9315,"duration_ms":90321,"concrete_test":"Take a representative sample of the HWMCC'19/'20 BMC instances from Section 4.1, run CaDiCaL 2.1.2 with proof logging enabled, and feed the emitted DRAT proofs to drat-trim (or a similar checker), classifying each added clause as RUP or RAT-only. If any RAT-only step is found, the DRAT-as-DRUP assumption fails and the Drup2Itp interpolation pipeline is not justified for that input; in that case, also check the extracted interpolants with a SAT solver for A⇒I and I⇒¬B to confirm unsoundness.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim—that Avy with CaDiCaL+Drup2Itp outperforms Avy+Glucose—presupposes that the interpolants Drup2Itp hands to Avy are semantically correct. The paper's only support for this is the assertion in Section 4 that CaDiCaL 2.1.2 'does not actually produce RAT clauses, so we can safely treat the emitted proof as a DRUP proof.' No evidence is given for this assertion, and no independent validation of interpolant correctness (A⇒I, I⇒¬B) or of Avy's answers against known HWMCC statuses is reported. This matters because Drup2Itp's trim() and replay() procedures rely on the RUP property: each logged learned clause must be derivable by unit propagation. If any proof step is RAT but not RUP, the chain derivation Drup2Itp constructs is not a valid resolution derivation, so the interpolant computation is unsupported and the performance differences in Table 1 could reflect an unsound interpolation path rather than a genuine improvement. The magnitude of the claimed gains (e.g., one additional solved instance on HWMCC'19 for the Minimizer row) makes this an especially fragile foundation.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents Drup2Itp, an implementation of DRUP-based interpolant generation for the SAT solver CaDiCaL, built on CaDiCaL 2.0's Tracer API so that the SAT solver itself is not modified. The implementation is integrated into the bit-level model checker Avy, optionally with a proof-minimization step (Minimizer), and evaluated on the HWMCC'19 and HWMCC'20 benchmark sets against Avy with Glucose as the baseline. The paper reports aggregate runtime and solved-instance counts, and claims that the CaDiCaL/Drup2Itp configuration—especially with proof minimization—outperforms the Glucose-based vanilla Avy.","tokens_in":14765,"tokens_out":3845,"duration_ms":38210,"significance":"If the implementation is sound, the paper makes a useful engineering contribution: it brings a state-of-the-art SAT solver into interpolation-based model checking through a decoupled, maintainable proof-tracer interface, and it provides a public implementation that can be reused by the community. The use of the Tracer API and the independent proof database is a genuine architectural improvement over modifying the solver internals, and the evaluation over two HWMCC benchmark sets is a meaningful real-world test. However, the central performance claim rests on two load-bearing assumptions that are not substantiated in the manuscript: that CaDiCaL's emitted proofs can safely be treated as DRUP proofs, and that the interpolants handed to Avy are semantically correct. The experimental evidence is also thinner than the abstract suggests: the headline claim is only supported by the Minimizer configuration, and the reported differences in solved instances are small.","major_comments":[{"comment":"The statement 'in the latest version available at the time of writing (2.1.2), CaDiCaL does not actually produce RAT clauses, so we can safely treat the emitted proof as a DRUP proof' is load-bearing for the entire paper. The correctness of the trim() and replay() procedures described in Section 3.1 depends on every logged clause having the RUP property: if any proof step is RAT but not RUP, the chain derivation constructed by Drup2Itp need not be a valid resolution derivation, and the interpolant computation is unsupported. No evidence is given for this claim, such as instrumentation showing that no RAT clauses occur, a version-specific check, or a proof-format validation on the benchmark instances. This must be addressed by either verifying the RUP property of every replayed step, disabling all RAT-producing techniques and arguing that the emitted proof is then DRUP, or adding explicit DRAT support.","section":"Section 4, paragraph 1"},{"comment":"The paper reports no direct validation that the interpolants produced by Drup2Itp satisfy the Craig conditions (A |= I and I |= ¬B) or even that they are well-formed formulas over the common variables. Since Table 1 only reports solved-instance counts and runtimes, an unsound interpolation path could produce spurious answers and faster solves without being detected. This is especially important because Avy relies on sequence interpolants for correctness. The authors should validate interpolants on a sample of the benchmark runs—for example, by checking A ∧ ¬I and I ∧ B with a SAT solver—or otherwise demonstrate that Avy's answers agree with known HWMCC statuses where available.","section":"Section 4.1 and Algorithms 2-3"},{"comment":"The abstract and Section 1 claim that integrating CaDiCaL with DRUP-based interpolants into Avy gives better performance than Avy with Glucose 'both in runtime and number of solved instances.' Table 1 does not support this claim for the plain CaDiCaL configuration: on HWMCC'19 it solves 203 instances versus Glucose's 205 and has a higher average runtime (1504.6 s versus 1447.5 s). The claim is only defensible for the Minimizer configuration (206 versus 205 on HWMCC'19, and 206 versus 201 on HWMCC'20). The paper should restrict its headline claim accordingly and provide per-instance comparison data or a statistical argument, since the total solved-instance differences are small and the average runtimes are influenced by many timeout-dominated values.","section":"Section 4.1, Table 1"}],"minor_comments":[{"comment":"There is a typo in 'unsatisifiable instance'; it should be 'unsatisfiable instance.'","section":"Section 1, paragraph 2"},{"comment":"The phrase 'to ensure a a DRUP proof is emitted' contains a duplicated article and should read 'to ensure a DRUP proof is emitted.'","section":"Section 4, paragraph 1"},{"comment":"Several figure captions read 'HMWCC' instead of 'HWMCC'; these should be corrected for consistency.","section":"Figure 6 captions"},{"comment":"The title of the cited paper by Gurfinkel and Vizel is rendered as 'Druping for interpolates'; the actual title is 'Druping for Interpolants.'","section":"Reference [13]"},{"comment":"The phrase 'under the diagonal of parity' is unclear; it should be 'below the diagonal' or 'below the diagonal of equality.'","section":"Figure 4 caption"}],"recommendation":"major_revision","confidential_remarks":"For the editor: the RAT-versus-DRUP concern is not a purely theoretical nit—it is the correctness foundation of the interpolant computation, and the manuscript's only response is an unverified assertion about a specific CaDiCaL version. That said, the issue is fixable with additional validation, and the engineering contribution is real. The empirical case would be strengthened by restricting the headline to the Minimizer configuration and by reporting any form of independent correctness check of the interpolants or the model-checking results. I do not see evidence of bad faith or circular benchmarking; the comparison is against a real baseline on standard benchmarks."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThis is a solid tool paper, not a conceptual breakthrough. The new thing is the implementation of the known DRUP interpolation algorithm from Gurfinkel and Vizel (FMCAD 2014) on top of CaDiCaL 2.0's Tracer API, so the SAT solver itself doesn't need modification. The Minimizer heuristic—re-solving the core and trimming again—is a sensible addition. The code is public, the design is clean, and the evaluation is honest: Avy with CaDiCaL+Drup2Itp-Minimizer solves 206 vs 205 on HWMCC'19 and 206 vs 201 on HWMCC'20 compared to Avy+Glucose. Those gains are modest but consistently positive, and the virtual-best numbers suggest headroom. The Section 4.2 study of proof and interpolant sizes is a welcome extra; it supports the claim that Minimizer helps.\n\nThe real soft spot is the DRAT-as-DRUP assumption. Section 4 says CaDiCaL 2.1.2 'does not actually produce RAT clauses,' so the emitted proof is treated as DRUP. That is an empirical claim about the solver's internals, and the paper gives no evidence—no proof-log inspection, no check with a DRAT checker, no statement that RAT-producing inprocessing was disabled. Since Drup2Itp's trim() and replay() depend on every logged clause being derivable by unit propagation, a single RAT clause in a reaching-the-core proof would break the RUP guarantee and could yield an unsound interpolant. The stress-test note is on target here. The authors should either verify that the emitted proofs are DRUP (or disable RAT-producing transformations) or validate the interpolants directly. There is also no check of Avy's answers against known HWMCC statuses; the evaluation is purely performance-based. That is acceptable in a tool paper, but it makes the modest gains harder to trust.\n\nA second, smaller issue: the comparison is against a single baseline, Avy with Glucose. No comparison with MiniSAT-based Avy or other interpolation paths, so part of the gain may simply be CaDiCaL being faster than Glucose on these benchmarks. Separating solver speed from interpolation overhead would strengthen the claim.\n\nWho benefits: people building interpolation-based model checkers or proof-consuming tools. They get a working, public implementation and a clear description of the engineering choices. This deserves a serious referee—the tool is real and the evaluation is fair, but the soundness assumption needs attention and the baseline set should be widened. I'd send it to review with that request.","headline":"A genuinely useful engineering contribution--DRUP interpolation on CaDiCaL's Tracer API--whose soundness rests on an unverified DRAT-as-DRUP assumption that a referee should push on.","tokens_in":15309,"tokens_out":3351,"would_cite":true,"duration_ms":33248,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper claims that DRUP-based interpolants can be generated in CaDiCaL 2.0 via its Tracer API without modifying the solver, and that doing so improves the performance of the model checker Avy on hardware verification benchmarks.","keywords":["DRUP proofs","Craig interpolation","CaDiCaL","SAT-based model checking","Avy","proof trimming","proof minimization","Tracer API"],"falsifier":"Take a sample of UNSAT formula pairs from the HWMCC benchmarks, compute Drup2Itp's interpolant, and check the Craig interpolant conditions: that the interpolant is implied by the A-side, contradicts the B-side, and uses only common variables; a single violation would falsify the implementation's correctness and, with it, the performance claim's foundation.","tokens_in":14321,"feed_emoji":"🔧","tokens_out":5780,"duration_ms":47951,"temperature":0.7,"pith_summary":"The paper claims that DRUP-based interpolants can be generated inside CaDiCaL 2.0 using its new Tracer API, with no changes to the SAT solver itself, and that this implementation, called Drup2Itp, improves the performance of the interpolation-based model checker Avy. On the HWMCC'19 and HWMCC'20 benchmark suites, Avy with CaDiCaL and Drup2Itp solves more instances and runs faster on average than Avy with Glucose as its solver. The work matters because interpolants are a key ingredient in SAT-based model checking, and CaDiCaL is one of the strongest available SAT solvers, so bringing interpolation to it broadens the toolkit for verification tools. A secondary claim is that proof minimization, which re-solves only the core of the proof before computing an interpolant, substantially shrinks both proof size and interpolant computation time in incremental settings.","feed_headline":"CaDiCaL-based interpolants beat Glucose in model checker Avy","feed_subtitle":"A DRUP-based interpolant generator on CaDiCaL's Tracer API lets Avy solve more hardware-verification benchmarks in less time.","key_machinery":"The load-bearing mechanism is the DRUP proof stack maintained by Drup2Itp, together with its trim()/replay() two-phase procedure. trim() walks the proof backwards, revives deleted clauses, and marks as core every clause that is needed to re-derive the empty clause by reverse unit propagation; replay() walks the core forward, re-derives each core clause by chain resolution, and feeds the resolution steps to a ResolutionProofIterator that computes interpolants on the fly. Proof minimization is carried by the Minimizer class, which collects the original core clauses, solves them with a fresh CaDiCaL instance, and computes the interpolant from the minimized proof. The Tracer API is what makes this possible without modifying the solver: it provides callbacks for clause addition and deletion, and Drup2Itp uses clause identifiers to keep its database synchronized with CaDiCaL's.","core_discovery":"The central discovery is an architecture in which an external class, Drup2Itp, plugs into CaDiCaL 2.0's Tracer API and maintains its own DRUP proof, clause database, unit-propagation engine, and conflict analysis. When the solver derives the empty clause, Drup2Itp trims the proof by marking the clauses that actually participate in the derivation of the empty clause, then replays the trimmed proof forward and reports resolution steps to an interpolation routine through a ResolutionProofIterator. The paper reports that when this machinery is integrated into Avy, the resulting configuration outperforms the existing Avy with Glucose in both runtime and number of solved instances on the HWMCC benchmarks, and that the optional Minimizer component further improves interpolant computation time and reduces interpolant size in incremental solving.","pith_inferences":["The reported gain may partly reflect CaDiCaL's raw solver strength rather than the DRUP interpolation method itself, since the comparison is against Glucose as a different solver; a controlled comparison would isolate the interpolation machinery.","The same Tracer-API design could be extended to DRAT and LRAT proofs with minimal new engineering, which would let interpolation coexist with proof-of-unsatisfiability certification.","Color-ordered propagation, which the paper mentions only as a heuristic for producing CNF-friendly interpolants, could be studied as a tunable parameter for interpolant quality in other model checkers.","The minimization step re-solves a core subset; on harder benchmarks where the core is not much smaller than the original, the overhead of an extra solve could outweigh the benefit, so the gain may be benchmark-dependent."],"forward_implications":["CaDiCaL becomes usable in any interpolation-based verification workflow, not just Avy, since Drup2Itp is solver-decoupled.","Proof minimization via Minimizer reduces both the replayed proof size and the resulting interpolant size in most incremental cases, which can speed up iterative model-checking loops.","The decoupling means future CaDiCaL releases can be supported without modifying solver internals, as long as the Tracer API remains stable.","The virtual-best score across CaDiCaL configurations exceeds any single configuration, suggesting that instance-specific configuration tuning could yield further gains.","The same trimming and replay machinery can be reused for unsat core extraction, which benefits abstraction-refinement and counterexample-guided refinement."],"supporting_citations":[{"why":"Supplies the original DRUP-based interpolation algorithm that Drup2Itp implements.","marker":"[13]"},{"why":"Introduces the CaDiCaL 2.0 Tracer API that the implementation builds on.","marker":"[4]"},{"why":"Defines Avy's interpolating property-directed reachability algorithm that consumes sequence interpolants.","marker":"[24]"},{"why":"Defines sequence interpolants used by Avy.","marker":"[23]"},{"why":"Establishes the RUP property and forward/backward validation that trim() relies on.","marker":"[12]"},{"why":"Provides the trimming and backward-validation technique and the core-marking scheme.","marker":"[14]"},{"why":"The McMillan interpolation system used to compute interpolants from resolution proofs.","marker":"[20]"},{"why":"Avy's fast interpolating BMC variant, part of the model-checking context.","marker":"[25]"}],"fun_headline_variants":["Avy gets faster with CaDiCaL DRUP interpolants","CaDiCaL 2.0 interpolants speed up model checking","DRUP interpolants on CaDiCaL beat Glucose in Avy","New interpolant engine pushes Avy past Glucose","CaDiCaL Tracer API enables faster Avy verification"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The performance claim rests on a single comparison between Avy-with-CaDiCaL/Drup2Itp and Avy-with-Glucose on the HWMCC benchmarks, and on the unstated assumption that Drup2Itp's interpolants are correct, since no explicit correctness validation of the interpolants is reported.","fun_headline_variants_meta":{"raw":{"variants":["Avy gets faster with CaDiCaL DRUP interpolants","CaDiCaL 2.0 interpolants speed up model checking","DRUP interpolants on CaDiCaL beat Glucose in Avy","New interpolant engine pushes Avy past Glucose","CaDiCaL Tracer API enables faster Avy verification"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000573,"raw_usage":{"total_tokens":2697,"prompt_tokens":926,"completion_tokens":1771,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":542,"completion_tokens_details":{"reasoning_tokens":1683}},"tokens_in":542,"tokens_out":1771,"duration_ms":11934,"temperature":1.0,"reasoning_tokens":1683,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T22:07:02.677085+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a sample of UNSAT formula pairs from the HWMCC benchmarks, compute Drup2Itp's interpolant, and check the Craig interpolant conditions: that the interpolant is implied by the A-side, contradicts the B-side, and uses only common variables; a single violation would falsify the implementation's correctness and, with it, the performance claim's foundation.","supporting_citations":[{"cited_title":"In: Formal Methods in Computer- Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014","cited_arxiv_id":null,"evidence_quote":"Supplies the original DRUP-based interpolation algorithm that Drup2Itp implements."},{"cited_title":"In: Gurfinkel, A., Ganesh, V","cited_arxiv_id":null,"evidence_quote":"Introduces the CaDiCaL 2.0 Tracer API that the implementation builds on."},{"cited_title":"In: Biere, A., Bloem, R","cited_arxiv_id":null,"evidence_quote":"Defines Avy's interpolating property-directed reachability algorithm that consumes sequence interpolants."},{"cited_title":"In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013","cited_arxiv_id":null,"evidence_quote":"Provides the trimming and backward-validation technique and the core-marking scheme."},{"cited_title":"In: Proceedings of the 15th International Conference on Computer Aided Verification (CA V)","cited_arxiv_id":null,"evidence_quote":"The McMillan interpolation system used to compute interpolants from resolution proofs."},{"cited_title":"In: Kroening, D., Pasareanu, C.S","cited_arxiv_id":null,"evidence_quote":"Avy's fast interpolating BMC variant, part of the model-checking context."}],"review_version":1}