This module contains the implementation of the LRAT checker as well as a proof that the given CNF is unsat if the checker succeeds.

def Std.Tactic.BVDecide.LRAT.check (lratProof : Array IntAction) (cnf : Sat.CNF Nat) : Bool

Check whether lratProof is a valid LRAT certificate for the unsatisfiability of cnf.

Equations

• Std.Tactic.BVDecide.LRAT.check lratProof cnf = Std.Tactic.BVDecide.LRAT.Internal.check lratProof cnf

theorem Std.Tactic.BVDecide.LRAT.check_sound (lratProof : Array IntAction) (cnf : Sat.CNF Nat) : check lratProof cnf = true → cnf.Unsat

If the check functions succeeds on lratProof and cnf then the cnf is unsatisfiable.