This adds the LRAT trimming algorithm from lrat-trim. Trimming is done by the bv_decide? tactic, such that the bv_check call that comes out of it uses a trimmed LRAT file for subsequent proof checking.
The algorithm is motivated by the fact that SAT solvers merely dump their CDCL execution log as an LRAT proof. This means that there are potentially a lot of proof steps that are actually unnecessary in the generated proof. The algorithm performs a use-def analysis of proof steps, starting at the empty clause in the end and working itself backwards. It then outputs a version of the proof that's only using the clauses that are actually necessary. According to data by the lrat-trim group this can often cut proof sizes by 30-40 percent.
Trying this on Eval.Popcount reduced the time spent in the kernel (This time consists of verifying the reflection step + bitblasting + Tseitin transformation + LRAT parsing + LRAT checking) from 1.4s to 0.4s on my machine.
Closes #80.
This adds the LRAT trimming algorithm from
lrat-trim. Trimming is done by thebv_decide?tactic, such that thebv_checkcall that comes out of it uses a trimmed LRAT file for subsequent proof checking.The algorithm is motivated by the fact that SAT solvers merely dump their CDCL execution log as an LRAT proof. This means that there are potentially a lot of proof steps that are actually unnecessary in the generated proof. The algorithm performs a use-def analysis of proof steps, starting at the empty clause in the end and working itself backwards. It then outputs a version of the proof that's only using the clauses that are actually necessary. According to data by the
lrat-trimgroup this can often cut proof sizes by 30-40 percent.Trying this on
Eval.Popcountreduced the time spent in the kernel (This time consists of verifying the reflection step + bitblasting + Tseitin transformation + LRAT parsing + LRAT checking) from 1.4s to 0.4s on my machine.