Module lrat 

LRAT refutations at scale: hint chains found by watched-literal propagation, trimmed to the clauses a refutation uses, and replayed by a checker that trusts nothing the search did.

A CDCL solve leaves its learned clauses in order, each derivable by reverse unit propagation (RUP) from the formula and the clauses before it (crate::cdcl::Solver::learned). crate::rup::check_refutation replays such a trace by propagating the whole database to a fixpoint for every clause, a cost a circuit miter of tens of thousands of clauses cannot pay a learned clause. refutation instead finds each clause’s LRAT hint chain (Cruz-Filipe et al., 2017) with two watched literals (Moskewicz et al., Chaff, 2001), walking the trace backward from the empty clause, the drat-trim order (Wetzler, Heule & Hunt, 2014): a learned clause no later step uses is never checked and never shipped. check replays a proof in time linear in its hints, and Lrat::to_text prints the standard LRAT text that crate::proof_emit::check_lrat and cake_lpr read. derivation trims the same way back from any target clauses of a log, not only the empty one — what one incremental solver derives across many queries — and check_derivation replays it and finds each target.

Ids follow the LRAT convention: the formula’s clauses are 1..=n in order, the j-th learned clause is n + 1 + j, and the empty clause takes the id after the last learned one. A trimmed proof skips the ids of the clauses it drops.

Structs

Lrat

An LRAT refutation of a formula whose clauses carry the ids 1..=n: additions in increasing id order, ending in the empty clause.

LratStep

One addition of an LRAT refutation: under the clause’s negation each hinted clause, in order, is unit, until the last conflicts.

Functions

check

Whether proof refutes original: every step’s id exceeds the one before it (and the formula’s), every hint names a clause already present, every step’s hints replay (each unit under the step’s negation, the last a conflict), and a step derives the empty clause. Every literal must lie below num_vars.

check_derivation

Whether proof derives every clause of claims from original: every step’s id exceeds the one before it (and the formula’s), every hint names a clause already present, every step’s hints replay, and each claim, its literals in any order, is the clause of a step or of the formula. Every literal must lie below num_vars.

derivation

The trimmed LRAT derivation of the clauses of log that targets names (by index) from original, every clause of log RUP from the formula and the clauses before it: a step for each target and for each log clause a step it leans on needs, in log order, the j-th log clause numbered after the formula’s. None when a target, or a clause one needs, is not RUP in its place, or a target names no log clause.

refutation

The trimmed LRAT refutation of original that learned (each clause RUP from the formula and the clauses before it) carries to the empty clause, or None when the empty clause is not RUP from them all or a learned clause the refutation needs is not RUP in its place: the derivation of the empty clause, after the learned clauses.