OTF performance examples - Walnut-Theorem-Prover/Walnut GitHub Wiki

Here are some examples where the OTF algorithms significantly outperform standard Subset Construction. Many more can be found in our OTF benchmark GitHub.

Note that several of these perform much better in more recent versions of Walnut. But even then, OTF outperforms Subset Construction.

• agrees from http://dx.doi.org/10.4153/S0008414X23000342
  • <1s, < 16GB with OTF-CCLS, versus ~87,000s and 120GB with Subset Construction
• co5no0 from https://arxiv.org/pdf/2503.04122
  • ~1s, < 16GB with OTF-CCLS, versus unknown with Subset Construction
• jaef from https://arxiv.org/abs/2503.01026
  • ~275s, ~70GB with OTF-CCLS, versus array overflow with Subset Construction
• pisotfaceeq from https://arxiv.org/abs/2206.01776
  • <1,000s, < 50GB with BRZ, OTF-BRZ-CCL, or OTF-BRZ-CCLS, versus unknown with hours and 5TB with Subset Construction
• pisotlargepow from https://arxiv.org/abs/2206.01776
  • <10s, < 16GB with OTF-CCLS, versus 1,200s and 90GB with Subset Construction
• testXXXX systems from https://arxiv.org/abs/2310.15064
  • 50-100s, < 16GB with OTF-CCLS, versus ~75,000s and 350GB with Subset Construction
• tribfaceeq from https://cs.uwaterloo.ca/~shallit/Talks/simons3.pdf
  • <2s, < 15GB with OTF-BRZ-CCLS, versus days of computation with Subset Construction