search

Gbury / mSAT

A modular sat/smt solver with proof output.
https://gbury.github.io/mSAT/
Apache License 2.0
95 stars 8 forks source link

wip: improve proof checking perf #17

Closed c-cube closed 5 years ago

c-cube commented 5 years ago

I changed the implementation to not used sorted lists and merge, but mutable atoms.

A stronger improvement could be gained by staying at the hyper-resolution level even during checking (possibly exposing a per-step expansion into pure resolution for backends that need it). See for example mc2's proof which computes pivot for each step of hyper-res, but doesn't store the (possibly big) intermediate clauses.

c-cube commented 5 years ago

Note: proofs are not stored properly in some cases (hole8.cnf for instance). I suspect that 0-levels resolutions are wrongly skipped when the unsat conflict comes from propagation (rather than learning the empty clause). Please don't merge yet, but discussions welcome ready to merge!