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 Std.Tactic.BVDecide.LRAT.IntAction) (cnf : Std.Sat.CNF Nat) :
Bool

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Std.Tactic.BVDecide.LRAT.check_sound (lratProof : Array Std.Tactic.BVDecide.LRAT.IntAction) (cnf : Std.Sat.CNF Nat) :
    Std.Tactic.BVDecide.LRAT.check lratProof cnf = true → cnf.Unsat

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