Hacker News Reader

I would have thought the SMT queries would be the most time-consuming part of this, but the authors make a big deal of leveraging Datalog optimzations to drive performance.

Especially given they purposefully don't re-use the SMT context across SMT terms.

Aren't the big SMT solvers already doing a bunch of optimization to allow incremental (push/pop) queries to be fast?

View on HN

We do use incremental solving. check-sat-assuming is generally better than push/pop, though, because Datalog's bottom-up search isn't DFS.

If you're interested, check out our ICLP 2020 extended abstract: https://cs.pomona.edu/~michael/papers/iclp2020_extabs.pdf. We should have more on this in not too long.

Super interesting, and cool technique. Do you have any insight into why CSA outperforms PP so often? I would have assumed the solvers were tuned for PP

I think the solvers _are_ tuned for PP. But we're comparing CSA and PP on the queries that Formulog issues... which don't really match well with the DFS discipline that the PP stack aligns with. I think CSA beats PP in our experiments because CSA is more flexible about locality.

Broadly---and I haven't looked at the memory usage to confirm this---I think CSA trades space (cache more old formulae, not just the prefix of some stack) for time (look, our answers are in the cache!).

Reply on news.ycombinator.com