equiv_receipt.rup

Forward DRAT checking — standard library only.

A DRAT refutation is a sequence of clause additions and deletions. An addition is sound if the added clause is reverse unit propagation (RUP): assuming the negation of every literal in the clause and propagating over the currently active clause set yields a conflict. Failing that, it may still be a resolution asymmetric tautology (RAT) on its first literal, which is what solvers emit when they eliminate variables.

Checking that is a few hundred lines. Producing it is what a SAT solver is for. That asymmetry is the whole reason this file exists: anyone can check, nobody has to trust.

Two implementations, on purpose. bcp() is the naive one: a few dozen lines, obviously correct, re-scanning every clause until nothing changes. It is the specification. ClauseDB is the fast one, using two watched literals per clause and an index for deletion, and it is what forward_rup_check() actually runs. They are checked against each other on random instances, so the fast path has an executable oracle rather than a promise.

Clause = typing.List[int]

def bcp( clauses: Sequence[List[int]], assumed: Sequence[int]) -> Tuple[bool, Dict[int, bool]]:

Unit propagation. Returns (conflict, assignment).

conflict is True when propagation derives a contradiction.

class MalformedProof(builtins.ValueError):

A DRAT text that cannot be parsed. Raised only by strict callers.

def parse_drat(drat_text: str) -> List[Tuple[str, List[int]]]:

Parse DRAT into ("a"|"d", clause) steps. Comment lines (c) are skipped.

Raises MalformedProof on unparseable input. Callers that must not crash should use forward_rup_check(), which converts this into a rejection — an unreadable proof proves nothing, which is a verdict, not an error condition.

class ClauseDB:

A clause store with two watched literals per clause.

The naive checker re-scans every active clause on every propagation round, and the active set grows by one on every lemma — so the cost of checking a proof grows worse than the product of its two dimensions. Watching two literals per clause means a clause is only visited when one of the two literals it is watching becomes false, which is what makes long proofs checkable.

The watch invariant survives between calls because every call propagates from an empty assignment and undoes nothing: there is no backtracking to invalidate.

ClauseDB(clauses: Sequence[List[int]] = ())

cl: List[List[int]]

watch: Dict[int, List[int]]

units: List[int]

deleted: set

index: Dict[Tuple[int, ...], List[int]]

has_empty

def add(self, lits: Sequence[int]) -> int:

def delete(self, lits: Sequence[int]) -> bool:

Mark one clause with exactly these literals deleted. False if absent.

Deletion is lazy: the index entry is dropped and the clause is added to a deleted set that propagation skips. Removing it from its two watch lists eagerly would cost more than skipping it.

def live(self):

The currently active clauses, in insertion order.

def propagate(self, assumed: Sequence[int]) -> Tuple[bool, Dict[int, bool]]:

Unit propagation from assumed. Returns (conflict, assignment).

Semantics are identical to bcp(); only the cost differs.

Truth is tracked as a set of true literals rather than a variable-to-bool map. "Is this literal true" becomes one set lookup and "is it false" becomes one on its negation, which removes an abs() and a second lookup from the innermost loop — measurably the hottest path in the file.

def forward_rup_check(clauses: Sequence[List[int]], drat_text: str) -> dict:

Verify a DRAT refutation by forward RUP checking.

Returns a dict with verified, n_lemmas, and — on failure — the failed_lemma and its zero-based failed_index so the defect is locatable rather than merely reported.

A refutation is accepted when an empty clause is derived, or when the final active set propagates to a conflict with no assumptions.