Module rup 

The RUP (Reverse Unit Propagation) linear checker — the fast default trust tier.

Modern certified SAT separates an untrusted, fast solver from a tiny, auditable checker that replays the solver’s resolution proof by unit propagation alone (Goldberg & Novikov, 2003 — RUP; Wetzler/Heule/Hunt, 2014 — DRAT; Cruz-Filipe et al., 2017 — LRAT; Tan/Heule/ Myreen, 2021 — the formally-verified cake_lpr). A learned clause C is valid iff assuming ¬C and unit-propagating the current clause database hits a conflict; the refutation is verified iff, after adding every learned clause in order, unit propagation over the whole database derives the empty clause.

This module re-derives NOTHING symbolic and builds no proof tree — so it sidesteps the emit-cost wall that sank eager probing. The solve produces the learned-clause trace for free (crate::cdcl::Solver::learned); here we check it, independently of the solver. The checker is deliberately small and naive (linear, fixpoint unit propagation) — its simplicity IS the trust. If it cannot confirm the solver’s UNSAT, we fail closed.

Enums

Verdict

A certified propositional entailment verdict.

Functions

check_refutation

Verify a DRAT/LRAT-style refutation: every learned clause is RUP w.r.t. the database built so far, and the full database is then refuted by unit propagation (the empty clause is RUP). Returns false if any step does not check — so a corrupted or bogus trace is rejected.

entails_certified

Decide premises ⊨ goal with the CDCL solver and independently certify an Entailed verdict by RUP replay. None if the problem is not purely propositional over recognisable atoms, OR if the solver claims UNSAT but the checker cannot confirm it (a solver bug — fail closed, never report a false Entailed).

entails_certified_prepared

Certify prepared ⊨ goal against a premise CNF clausified ONCE by Cnf::from_premises. Solving a whole puzzle this way pays the of-pair Tseitin cost a single time, then each cell only adds its ¬goal unit — the incremental win.