Implement LRAT proof certification for SAT Competition 2025

[Copilot]

Issue #303 tracks adding proof output support for SAT Competition 2025. This PR implements LRAT (Linear Resolution Asymmetric Tautologies) proof certification in splr, replacing the earlier DPR approach.

Key findings

• LRAT requires sequential clause IDs — every clause (input and learned) gets a monotonically increasing step ID; input clause IDs are implicit (known from the CNF file) while learned clause additions and deletions are written to the proof file with their IDs.
• CDCL learned clauses need UP-chain hints — the LRAT verifier uses the hint list to check each learned clause in linear time without re-running full unit propagation.
• BVE resolvents require RAT steps in LRAT — not yet implemented; the preprocessor is skipped when LRAT certification is active to ensure a valid proof.

Changes

• unsat_certificate.rs: Replaced the DRAT queue-based system with direct LRAT writes. Three methods: add_input_clause() allocates a step ID for original clauses without writing (LRAT verifier knows them from the CNF); add_clause_lrat(clause, hints) writes id lit* 0 hint* 0\n; delete_clause_lrat(id) writes step_id d clause_id 0\n. A no-op stub is provided for the no_IO feature.
• types/clause.rs: Added lrat_id: u64 field to Clause (gated on not(feature = "no_IO")) to track each clause's LRAT proof step ID.
• state.rs: Added lrat_hints: Vec<u64> to State (gated on not(feature = "no_IO")) for collecting antecedent clause IDs during conflict analysis.
• cdb/mod.rs (ClauseDBIF trait): Removed new_clause_pr/certificate_add_clause_pr; added new_clause_lrat(&mut self, asg, v, hints: &[u64]) -> RefClause, certificate_add_assertion_lrat(&mut self, lit, hints), and is_certification_active() -> bool.
• cdb/db.rs: new_clause calls add_input_clause() for original clauses and add_clause_lrat(v, &[]) for other learnt clauses; new_clause_lrat writes with proper hints; new_clause_store accepts and stores the lrat_id; all transform functions (transform_by_elimination, transform_by_replacement, transform_by_simplification) save the old LRAT ID before in-place modification and assign a new one after; remove_clause_fn deletes by LRAT ID via delete_clause_lrat(c.lrat_id).
• solver/conflict.rs: conflict_analyze clears state.lrat_hints at the start and collects antecedent LRAT IDs — cdb[cid].lrat_id for Implication(cid) reasons and the matching binary clause ID (via cdb.binary_links) for BinaryLink(l) reasons. handle_conflict uses new_clause_lrat for multi-literal learned clauses and certificate_add_assertion_lrat for unit learned clauses, both with the collected hints.
• processor/eliminate.rs: Reverted to plain new_clause (BVE is skipped when certification is active).
• solver/search.rs: Added !cdb.is_certification_active() guard on the preprocessing elimination step so BVE is skipped when LRAT output is requested.
• config.rs: Updated help/doc strings from "DPR" → "LRAT"; default output filename remains proof.out.

Testing

• All 14 unit tests and 20 doc tests pass.
• Clean build with and without the no_IO feature flag.
• CodeQL security scan: 0 alerts.

---

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.

[Copilot]

Just as a heads up, I was blocked by some firewall rules while working on your feedback. Expand below for details.

Warning

Firewall rules blocked me from connecting to one or more addresses (expand for details)

I tried to connect to the following addresses, but was blocked by firewall rules:

• satcompetition.github.io
  • Triggering command: /home/REDACTED/work/_temp/ghcca-node/node/bin/node /home/REDACTED/work/_temp/ghcca-node/node/bin/node --enable-source-maps /home/REDACTED/work/_temp/copilot-developer-action-main/dist/index.js (dns block)

If you need me to access, download, or install something from one of these locations, you can either:

• Configure Actions setup steps to set up my environment, which run before the firewall is enabled
• Add the appropriate URLs or hosts to the custom allowlist in this repository's Copilot coding agent settings (admins only)

[shnarazk]

@copilot No files have been updated. What's up?

[Copilot]

@copilot No files have been updated. What's up?

Done in fc6a296. The DPR proof format is now implemented:

• CertificationStore::add_clause_pr(clause, witness) — writes a DPR PR step directly to the proof file as l1 l2 ... lk 0 w1 w2 ... wm 0, flushing any queued DRAT lines first to preserve ordering
• ClauseDBIF::new_clause_pr — new trait method for creating BVE resolvent clauses with a PR witness
• eliminate_var — uses new_clause_pr with Lit::from((vi, true)) as the witness (the pivot variable's positive literal), since the resolvent of (v ∨ p1 ∨ … ∨ pk) and (¬v ∨ n1 ∨ … ∨ nm) is RAT with witness {v}
• config.rs — default proof filename changed from proof.drat → proof.out (SAT Comp 2025 requirement), help text updated DRAT → DPR

CDCL learned clauses remain as plain RUP lines (valid DPR with no witness needed), so the proof format is fully backwards compatible with dpr-trim.

[shnarazk]

@copilot
Sorry re-plan this PR to implement LRAT certification instead of DPR.

[Copilot]

@copilot
Sorry re-plan this PR to implement LRAT certification instead of DPR.

Done in 9909974. The DPR implementation has been replaced with LRAT (Linear Resolution Asymmetric Tautologies) certification:

• CertificationStore: Replaced the DRAT queue with direct LRAT writes. Sequential next_step_id counter. add_input_clause() allocates an ID for original clauses without writing (LRAT verifier knows them from the CNF). add_clause_lrat(clause, hints) writes a full LRAT step. delete_clause_lrat(id) writes deletion by ID.
• Clause.lrat_id: Each clause now carries its LRAT proof step ID.
• Hint collection: conflict_analyze populates state.lrat_hints from antecedent clause IDs (both Implication(cid) and BinaryLink reasons), and handle_conflict passes these to new_clause_lrat.
• BVE: The preprocessor is skipped when LRAT certification is active (BVE resolvents would require RAT steps in LRAT, not yet implemented). Added is_certification_active() trait method for this guard in search.rs.
• All 14 unit tests + 20 doc tests pass; CodeQL: 0 alerts.

[shnarazk]

Summary of LRAT Certificate Bugs and Fixes

Bug 1: Input unit clauses written to proof file (Major — src/solver/build.rs)

Problem: When loading CNF clauses, unit input clauses called certificate_add_assertion() which wrote them to the LRAT proof file as derived clauses with no hints. Input clauses should NOT appear in the proof — the checker knows them from the CNF file.

Fix: Added add_input_clause() method that allocates an LRAT step ID for every CNF clause (including tautologies, satisfied clauses, and unit clauses) without writing to the proof file. Created a new new_clause_input() method for clauses with pre-allocated LRAT IDs.

Bug 2: Tautological/dead input clauses skip LRAT ID allocation (Major — src/solver/build.rs)

Problem: When a CNF clause was a tautology or already satisfied by unit propagation, add_unchecked_clause returned Dead without allocating an LRAT ID. This shifted all subsequent clause IDs, making hints reference wrong clauses.

Fix: In the new add_input_clause(), the LRAT ID is allocated unconditionally at the top of the function, before any simplification or filtering.

Bug 3: Incomplete LRAT hints from clause minimization (Major — src/solver/conflict.rs)

Problem: minimize_learnt removes redundant literals from learnt clauses by traversing the implication graph, but the LRAT hints for the traversed reason clauses were never collected.

Fix: Skip learnt clause minimization when LRAT certification is active (added find_backtrack_level function for computing backtrack level without minimization).

Bug 4: Empty hints for simplified clauses during root-level propagation (Moderate — src/assign/propagate.rs)

Problem: transform_by_simplification (called from propagate_at_root_level) wrote shortened clauses and new unit clauses to the LRAT proof with empty hints.

Fix: Skip propagate_at_root_level entirely when LRAT certification is active.

Bug 5: Binary clause hints not collected when variable already SEEN (Major — src/solver/conflict.rs)

Problem: In conflict analysis, LRAT hints for binary link reason clauses were only collected inside the if !CA_SEEN block. When the linked variable was already SEEN, the hint was silently dropped.

Fix: Moved LRAT hint collection for binary clauses OUTSIDE the !CA_SEEN check, so hints are always collected regardless of SEEN status.

Bug 6: LRAT hints in wrong order (Major — src/solver/conflict.rs)

Problem: Conflict analysis traverses the trail backwards, collecting hints in reverse propagation order. LRAT checkers expect hints in forward propagation order.

Fix: Reverse the non-root hints after collection. Root-level hints are placed first (since they represent unit clauses that must propagate before other clauses become unit).

Bug 7: Missing hints for root-level literals (Major — src/solver/conflict.rs, src/state.rs)

Problem: Root-level literals were skipped during conflict analysis (if root_level == lvl { continue; }), meaning the clauses that justified their assignments were never included in LRAT hints. The LRAT checker needs these to verify the derivation.

Fix: Added lrat_root_ids: Vec<u64> to State to track the LRAT step ID for each root-level variable assignment. During conflict analysis, when a root-level literal is encountered, its justification clause ID is added to the hints.

Bug 8: Missing empty clause in LRAT proof (Major — src/solver/build.rs)

Problem: The LRAT proof never contained a derivation of the empty clause. LRAT checkers require an explicit empty clause step to verify the proof is complete.

Fix: In save_certification, emit the empty clause with all root-level LRAT IDs as hints before closing the proof file.

Bug 9: Missing hints from pure literal elimination and vivification

Problem: Pure literal elimination (search.rs) and vivification (vivify.rs) call certificate_add_assertion without LRAT hints.

Fix: Skip pure literal elimination and vivification when LRAT certification is active (similar to how the eliminator was already disabled).