4 ms·
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
by mgreenbe 6y ago
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 https://cs.pomona.edu/~michael/papers/iclp2020_extabs.pdf. We should have more on this in not too long.
- fovc 6y agoSuper 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
- mgreenbe 6y agoI 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!).