This module implements the LRAT trimming algorithm described in section 4 of "Faster LRAT Checking Than Solving with CaDiCaL" (https://drops.dagstuhl.de/storage/00lipics/lipics-vol271-sat2023/LIPIcs.SAT.2023.21/LIPIcs.SAT.2023.21.pdf).
- used : ByteArray
For each proof step
i
contains at indexi - initialId
0
ifi
is unused,1
if it is used. For each proof step
i
contains at indexi - initialId
the step thati
maps to in the new proof or0
if that step is not yet set. Used such that the proof remains a sequence without gaps.
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Perform a use-def analysis of LRAT proof steps, starting at the empty clause and working its way up with DFS.
Equations
Instances For
Map the set of used proof steps to a new LRAT proof that has no holes in the sequence of proof identifiers.
Equations
Instances For
Equations
Instances For
Trim the LRAT proof
by removing all steps that are not used in reaching the empty clause
conclusion.