Documentation

Std.Tactic.BVDecide.LRAT.Checker

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

source
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
    Instances For
      source
      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.