search

leanprover / leansat

This package provides an interface and foundation for verified SAT reasoning
Apache License 2.0
48 stars 6 forks source link

Investigate `lrat-trim` #80

Closed hargoniX closed 3 months ago

hargoniX commented 3 months ago

https://github.com/arminbiere/lrat-trim can be useful for us in two ways:

  1. It provides a high performance LRAT checker implementation. We can probably check their algorithm out and learn something for our own verified implementation.
  2. It is capable of reducing the LRAT proof size considerably (Reference from Eval.Popcount: c trimmed 91256 added clauses in original proof to 56188 clauses 62%) running this as a post processing step could speed up verification further.
hargoniX commented 3 months ago

According to: https://drops.dagstuhl.de/storage/00lipics/lipics-vol271-sat2023/LIPIcs.SAT.2023.21/LIPIcs.SAT.2023.21.pdf the trimming is basically a depth first search followed by a renaming to keep indizes sequential. We might just be able to reimplement this in Lean and still cut down significantly on the size of the LRAT proofs.